Kolmogorov-Chentsov theorem #
theorem
UniformContinuousOn.exists_tendsto
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[FirstCountableTopology α]
[UniformSpace β]
[CompleteSpace β]
{s t : Set α}
(hs : Dense s)
(ht : IsOpen t)
{f : ↑s → β}
(hf : UniformContinuousOn f {x : ↑s | ↑x ∈ t})
(a : α)
(ha : a ∈ t)
:
∃ (c : β), Filter.Tendsto f (Filter.comap Subtype.val (nhds a)) (nhds c)
theorem
Dense.holderOnWith_extend
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
[CompleteSpace Y]
{C r : NNReal}
{s : Set X}
{f : ↑s → Y}
{U : Set X}
(hU : IsOpen U)
(hs : Dense s)
(hf : HolderOnWith C r f {x : ↑s | ↑x ∈ U})
(hr : 0 < r)
:
HolderOnWith C r (hs.extend f) U
theorem
UniformContinuous.exists_tendsto
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[FirstCountableTopology α]
[UniformSpace β]
[CompleteSpace β]
{s : Set α}
{f : ↑s → β}
(hf : UniformContinuous f)
(a : α)
(has : a ∈ closure s)
:
∃ (c : β), Filter.Tendsto f (Filter.comap Subtype.val (nhds a)) (nhds c)
theorem
measurable_limUnder_of_exists_tendsto
{ι : Type u_1}
{X : Type u_2}
{E : Type u_3}
{mX : MeasurableSpace X}
[TopologicalSpace E]
[TopologicalSpace.PseudoMetrizableSpace E]
[MeasurableSpace E]
[BorelSpace E]
{l : Filter ι}
[l.IsCountablyGenerated]
{f : ι → X → E}
[hE : Nonempty E]
(h_conv : ∀ (x : X), ∃ (c : E), Filter.Tendsto (fun (x_1 : ι) => f x_1 x) l (nhds c))
(hf : ∀ (i : ι), Measurable (f i))
:
Measurable fun (x : X) => limUnder l fun (x_1 : ι) => f x_1 x
theorem
measurable_limUnder
{ι : Type u_1}
{X : Type u_2}
{E : Type u_3}
[MeasurableSpace X]
[TopologicalSpace E]
[PolishSpace E]
[MeasurableSpace E]
[BorelSpace E]
[Countable ι]
{l : Filter ι}
[l.IsCountablyGenerated]
{f : ι → X → E}
[hE : Nonempty E]
(hf : ∀ (i : ι), Measurable (f i))
:
Measurable fun (x : X) => limUnder l fun (x_1 : ι) => f x_1 x
theorem
limUnder_prod
{α : Type u_1}
{β : Type u_2}
{X : Type u_3}
{Y : Type u_4}
[TopologicalSpace X]
[TopologicalSpace Y]
[Nonempty X]
[Nonempty Y]
[T2Space X]
[T2Space Y]
{f : Filter α}
{f' : Filter β}
[f.NeBot]
[f'.NeBot]
{g : α → X}
{g' : β → Y}
(h₁ : ∃ (x : X), Filter.Tendsto g f (nhds x))
(h₂ : ∃ (x' : Y), Filter.Tendsto g' f' (nhds x'))
:
def
ProbabilityTheory.holderSet
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[PseudoEMetricSpace T]
[EMetricSpace E]
(X : T → Ω → E)
(T' : Set T)
(p β : ℝ)
(U : Set T)
:
Set Ω
A set on which the process is Hölder continuous.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
ProbabilityTheory.IsKolmogorovProcess.measurableSet_holderSet
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{X : T → Ω → E}
{p q : ℝ}
{M β : NNReal}
{P : MeasureTheory.Measure Ω}
{U : Set T}
[PseudoEMetricSpace T]
[EMetricSpace E]
(hX : IsKolmogorovProcess X P p q M)
{T' : Set T}
(hT' : T'.Countable)
:
MeasurableSet (holderSet X T' p (↑β) U)
theorem
ProbabilityTheory.holderOnWith_of_mem_holderSet
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{X : T → Ω → E}
{c : ENNReal}
{d p : ℝ}
{β : NNReal}
{U : Set T}
[PseudoEMetricSpace T]
[EMetricSpace E]
(hT : HasBoundedInternalCoveringNumber U c d)
(hd_pos : 0 < d)
(hp_pos : 0 < p)
(hβ_pos : 0 < β)
{T' : Set T}
{ω : Ω}
(hω : ω ∈ holderSet X T' p (↑β) U)
:
theorem
ProbabilityTheory.uniformContinuousOn_of_mem_holderSet
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{X : T → Ω → E}
{c : ENNReal}
{d p : ℝ}
{β : NNReal}
{U : Set T}
[PseudoEMetricSpace T]
[EMetricSpace E]
(hT : HasBoundedInternalCoveringNumber U c d)
(hd_pos : 0 < d)
(hp_pos : 0 < p)
(hβ_pos : 0 < β)
{T' : Set T}
{ω : Ω}
(hω : ω ∈ holderSet X T' p (↑β) U)
:
theorem
ProbabilityTheory.continuousOn_of_mem_holderSet
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{X : T → Ω → E}
{c : ENNReal}
{d p : ℝ}
{β : NNReal}
{U : Set T}
[PseudoEMetricSpace T]
[EMetricSpace E]
(hT : HasBoundedInternalCoveringNumber U c d)
(hd_pos : 0 < d)
(hp_pos : 0 < p)
(hβ_pos : 0 < β)
{T' : Set T}
{ω : Ω}
(hω : ω ∈ holderSet X T' p (↑β) U)
:
theorem
ProbabilityTheory.exists_tendsto_of_mem_holderSet
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{X : T → Ω → E}
{c : ENNReal}
{d p : ℝ}
{β : NNReal}
{U : Set T}
[PseudoEMetricSpace T]
[EMetricSpace E]
[CompleteSpace E]
(hT : HasBoundedInternalCoveringNumber U c d)
(hU : IsOpen U)
(hd_pos : 0 < d)
(hp_pos : 0 < p)
(hβ_pos : 0 < β)
{T' : Set T}
(hT'_dense : Dense T')
{ω : Ω}
(hω : ω ∈ holderSet X T' p (↑β) U)
(t : T)
(htU : t ∈ U)
:
∃ (c : E), Filter.Tendsto (fun (t' : ↑T') => X (↑t') ω) (Filter.comap Subtype.val (nhds t)) (nhds c)
theorem
ProbabilityTheory.ae_mem_holderSet
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{X : T → Ω → E}
{c : ENNReal}
{d p q : ℝ}
{M β : NNReal}
{P : MeasureTheory.Measure Ω}
{U : Set T}
[PseudoEMetricSpace T]
[EMetricSpace E]
[MeasurableSpace E]
[BorelSpace E]
(hT : HasBoundedInternalCoveringNumber U c d)
(hX : IsKolmogorovProcess X P p q M)
(hc : c ≠ ⊤)
(hd_pos : 0 < d)
(hdq_lt : d < q)
(hβ_pos : 0 < β)
(hβ_lt : ↑β < (q - d) / p)
{T' : Set T}
(hT'_countable : T'.Countable)
:
theorem
ProbabilityTheory.IsKolmogorovProcess.tendstoInMeasure
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{X : T → Ω → E}
{p q : ℝ}
{M : NNReal}
{P : MeasureTheory.Measure Ω}
[PseudoEMetricSpace T]
[EMetricSpace E]
(hX : IsKolmogorovProcess X P p q M)
(hq_pos : 0 < q)
{T' : Set T}
{u : ℕ → ↑T'}
{t : T}
(hu : Filter.Tendsto (fun (n : ℕ) => ↑(u n)) Filter.atTop (nhds t))
:
MeasureTheory.TendstoInMeasure P (fun (n : ℕ) => X ↑(u n)) Filter.atTop (X t)
theorem
ProbabilityTheory.measurable_indicatorProcess
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{X : T → Ω → E}
[hE : Nonempty E]
{A : Set Ω}
[MeasurableSpace E]
(hA : MeasurableSet A)
(hX : ∀ (t : T), Measurable (X t))
(t : T)
:
Measurable (indicatorProcess X A t)
theorem
ProbabilityTheory.measurable_pair_indicatorProcess
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
[EMetricSpace E]
[hE : Nonempty E]
{T₁ : Type u_4}
{T₂ : Type u_5}
[MeasurableSpace E]
[BorelSpace E]
{X₁ : T₁ → Ω → E}
{X₂ : T₂ → Ω → E}
(hX₁ : ∀ (t : T₁), Measurable (X₁ t))
(hX₂ : ∀ (t : T₂), Measurable (X₂ t))
(hX₁₂ : ∀ (i : T₁) (j : T₂), Measurable fun (ω : Ω) => (X₁ i ω, X₂ j ω))
{A₁ A₂ : Set Ω}
(hA₁ : MeasurableSet A₁)
(hA₂ : MeasurableSet A₂)
(s : T₁)
(t : T₂)
:
Measurable fun (ω : Ω) => (indicatorProcess X₁ A₁ s ω, indicatorProcess X₂ A₂ t ω)
theorem
ProbabilityTheory.measurable_edist_indicatorProcess
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
[EMetricSpace E]
[hE : Nonempty E]
{T₁ : Type u_4}
{T₂ : Type u_5}
[MeasurableSpace E]
[BorelSpace E]
{X₁ : T₁ → Ω → E}
{X₂ : T₂ → Ω → E}
(hX₁ : ∀ (t : T₁), Measurable (X₁ t))
(hX₂ : ∀ (t : T₂), Measurable (X₂ t))
(hX₁₂ : ∀ (i : T₁) (j : T₂), Measurable fun (ω : Ω) => (X₁ i ω, X₂ j ω))
{A₁ A₂ : Set Ω}
(hA₁ : MeasurableSet A₁)
(hA₂ : MeasurableSet A₂)
(s : T₁)
(t : T₂)
:
Measurable fun (ω : Ω) => edist (indicatorProcess X₁ A₁ s ω) (indicatorProcess X₂ A₂ t ω)
theorem
ProbabilityTheory.measurable_pair_limUnder_comap
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace T]
[EMetricSpace E]
[hE : Nonempty E]
{X₁ X₂ : T → Ω → E}
{T' : Set T}
(hT'_dense : Dense T')
(hX₁₂ : ∀ (i j : T), Measurable fun (ω : Ω) => (X₁ i ω, X₂ j ω))
(s t : T)
(hX₁_tendsto :
∀ (ω : Ω), ∃ (x : E), Filter.Tendsto (fun (t' : ↑T') => X₁ (↑t') ω) (Filter.comap Subtype.val (nhds s)) (nhds x))
(hX₂_tendsto :
∀ (ω : Ω), ∃ (x : E), Filter.Tendsto (fun (t' : ↑T') => X₂ (↑t') ω) (Filter.comap Subtype.val (nhds t)) (nhds x))
:
Measurable fun (ω : Ω) =>
(limUnder (Filter.comap Subtype.val (nhds s)) fun (t' : ↑T') => X₁ (↑t') ω, limUnder (Filter.comap Subtype.val (nhds t)) fun (t' : ↑T') => X₂ (↑t') ω)
def
ProbabilityTheory.denseCountable
(T : Type u_4)
[TopologicalSpace T]
[SecondCountableTopology T]
:
Set T
A countable dense subset of a second-countable topological space.
Equations
Instances For
theorem
ProbabilityTheory.dense_denseCountable
{T : Type u_1}
[PseudoEMetricSpace T]
[SecondCountableTopology T]
:
Dense (denseCountable T)
theorem
ProbabilityTheory.countable_denseCountable
{T : Type u_1}
[PseudoEMetricSpace T]
[SecondCountableTopology T]
:
def
ProbabilityTheory.IsLimitOfIndicator
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace T]
[EMetricSpace E]
[hE : Nonempty E]
[SecondCountableTopology T]
(Y X : T → Ω → E)
(P : MeasureTheory.Measure Ω)
(U : Set T)
:
A class of processes built from an other. Used to ensure measurability.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
ProbabilityTheory.measurable_pair_limUnder_indicatorProcess
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace T]
[EMetricSpace E]
[hE : Nonempty E]
[MeasurableSpace E]
[BorelSpace E]
[SecondCountableTopology T]
{X X' : T → Ω → E}
(hX : ∀ (t : T), Measurable (X t))
(hX' : ∀ (t : T), Measurable (X' t))
(hX_pair : ∀ (i j : T), Measurable fun (ω : Ω) => (X i ω, X' j ω))
{A₁ A₂ : Set Ω}
(hA₁ : MeasurableSet A₁)
(hA₂ : MeasurableSet A₂)
(s t : T)
(h_tendsto₁ :
∀ ω ∈ A₁,
∃ (c : E),
Filter.Tendsto (fun (t' : ↑(denseCountable T)) => X (↑t') ω) (Filter.comap Subtype.val (nhds s)) (nhds c))
(h_tendsto₂ :
∀ ω ∈ A₂,
∃ (c : E),
Filter.Tendsto (fun (t' : ↑(denseCountable T)) => X' (↑t') ω) (Filter.comap Subtype.val (nhds t)) (nhds c))
:
Measurable fun (ω : Ω) =>
(limUnder (Filter.comap Subtype.val (nhds s)) fun (t' : ↑(denseCountable T)) => indicatorProcess X A₁ (↑t') ω, limUnder (Filter.comap Subtype.val (nhds t)) fun (t' : ↑(denseCountable T)) => indicatorProcess X' A₂ (↑t') ω)
theorem
ProbabilityTheory.IsLimitOfIndicator.measurable_pair
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[PseudoEMetricSpace T]
[EMetricSpace E]
[hE : Nonempty E]
[MeasurableSpace E]
[BorelSpace E]
[SecondCountableTopology T]
{Y X Z X' : T → Ω → E}
{U₁ U₂ : Set T}
(hX : ∀ (t : T), Measurable (X t))
(hX' : ∀ (t : T), Measurable (X' t))
(hX_pair : ∀ (i j : T), Measurable fun (ω : Ω) => (X i ω, X' j ω))
(hY : IsLimitOfIndicator Y X P U₁)
(hZ : IsLimitOfIndicator Z X' P U₂)
(s t : T)
:
Measurable fun (ω : Ω) => (Y s ω, Z t ω)
theorem
ProbabilityTheory.IsLimitOfIndicator.measurable
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{U : Set T}
[PseudoEMetricSpace T]
[EMetricSpace E]
[hE : Nonempty E]
[MeasurableSpace E]
[BorelSpace E]
[SecondCountableTopology T]
{Y X : T → Ω → E}
(hX : ∀ (t : T), Measurable (X t))
(hY : IsLimitOfIndicator Y X P U)
(t : T)
:
Measurable (Y t)
theorem
ProbabilityTheory.IsLimitOfIndicator.measurable_edist
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[PseudoEMetricSpace T]
[EMetricSpace E]
[hE : Nonempty E]
[MeasurableSpace E]
[BorelSpace E]
[SecondCountableTopology T]
{Y X Z X' : T → Ω → E}
{U₁ U₂ : Set T}
(hX : ∀ (t : T), Measurable (X t))
(hX' : ∀ (t : T), Measurable (X' t))
(hX_pair : ∀ (i j : T), Measurable fun (ω : Ω) => (X i ω, X' j ω))
(hY : IsLimitOfIndicator Y X P U₁)
(hZ : IsLimitOfIndicator Z X' P U₂)
(s t : T)
:
Measurable fun (ω : Ω) => edist (Y s ω) (Z t ω)
theorem
ProbabilityTheory.IsLimitOfIndicator.indicatorProcess
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{U : Set T}
[PseudoEMetricSpace T]
[EMetricSpace E]
[hE : Nonempty E]
[SecondCountableTopology T]
{Y X : T → Ω → E}
(hY : IsLimitOfIndicator Y X P U)
(A : Set Ω)
(hA_meas : MeasurableSet A)
(hA_ae : ∀ᵐ (ω : Ω) ∂P, ω ∈ A)
:
IsLimitOfIndicator (fun (t : T) => ProbabilityTheory.indicatorProcess Y A t) X P U
noncomputable def
ProbabilityTheory.holderModification
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[PseudoEMetricSpace T]
[EMetricSpace E]
[hE : Nonempty E]
[SecondCountableTopology T]
(X : T → Ω → E)
(β : NNReal)
(p : ℝ)
(U : Set T)
[DecidablePred fun (x : T) => x ∈ U]
:
T → Ω → E
A Hölder continuous modification of a process X.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
ProbabilityTheory.isLimitOfIndicator_holderModification
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{X : T → Ω → E}
{c : ENNReal}
{d p q : ℝ}
{M β : NNReal}
{P : MeasureTheory.Measure Ω}
{U : Set T}
[PseudoEMetricSpace T]
[EMetricSpace E]
[hE : Nonempty E]
[MeasurableSpace E]
[BorelSpace E]
[CompleteSpace E]
[SecondCountableTopology T]
(hT : HasBoundedInternalCoveringNumber U c d)
[DecidablePred fun (x : T) => x ∈ U]
(hU : IsOpen U)
(hX : IsKolmogorovProcess X P p q M)
(hc : c ≠ ⊤)
(hd_pos : 0 < d)
(hdq_lt : d < q)
(hβ_pos : 0 < β)
(hβ_lt : ↑β < (q - d) / p)
:
IsLimitOfIndicator (holderModification X β p U) X P U
theorem
ProbabilityTheory.holderModification_eq
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{X : T → Ω → E}
{c : ENNReal}
{d p q : ℝ}
{M β : NNReal}
{P : MeasureTheory.Measure Ω}
{U : Set T}
[PseudoEMetricSpace T]
[EMetricSpace E]
[hE : Nonempty E]
[SecondCountableTopology T]
(hT : HasBoundedInternalCoveringNumber U c d)
(hU : IsOpen U)
[DecidablePred fun (x : T) => x ∈ U]
(hX : IsKolmogorovProcess X P p q M)
(hd_pos : 0 < d)
(hβ_pos : 0 < β)
(t' : ↑(denseCountable T))
(ht'U : ↑t' ∈ U)
{ω : Ω}
(hω : ω ∈ holderSet X (denseCountable T) p (↑β) U)
:
theorem
ProbabilityTheory.exists_tendsto_indicatorProcess_holderSet
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{X : T → Ω → E}
{c : ENNReal}
{d p q : ℝ}
{M β : NNReal}
{P : MeasureTheory.Measure Ω}
{U : Set T}
[PseudoEMetricSpace T]
[EMetricSpace E]
[hE : Nonempty E]
[CompleteSpace E]
(hT : HasBoundedInternalCoveringNumber U c d)
(hU : IsOpen U)
(hX : IsKolmogorovProcess X P p q M)
(hd_pos : 0 < d)
(hβ_pos : 0 < β)
{T' : Set T}
(hT'_dense : Dense T')
(t : T)
(htU : t ∈ U)
(ω : Ω)
:
∃ (c : E),
Filter.Tendsto (fun (x : ↑T') => indicatorProcess X (holderSet X T' p (↑β) U) (↑x) ω)
(Filter.comap Subtype.val (nhds t)) (nhds c)
theorem
ProbabilityTheory.measurable_holderModification
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{X : T → Ω → E}
{c : ENNReal}
{d p q : ℝ}
{M β : NNReal}
{P : MeasureTheory.Measure Ω}
{U : Set T}
[PseudoEMetricSpace T]
[EMetricSpace E]
[hE : Nonempty E]
[MeasurableSpace E]
[BorelSpace E]
[CompleteSpace E]
[SecondCountableTopology T]
(hT : HasBoundedInternalCoveringNumber U c d)
[DecidablePred fun (x : T) => x ∈ U]
(hU : IsOpen U)
(hX : IsKolmogorovProcess X P p q M)
(hc : c ≠ ⊤)
(hd_pos : 0 < d)
(hdq_lt : d < q)
(hβ_pos : 0 < β)
(hβ_lt : ↑β < (q - d) / p)
(t : T)
:
Measurable (holderModification X β p U t)
theorem
ProbabilityTheory.measurable_pair_holderModification
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[PseudoEMetricSpace T]
[EMetricSpace E]
[hE : Nonempty E]
[MeasurableSpace E]
[BorelSpace E]
[CompleteSpace E]
[SecondCountableTopology T]
{U₁ U₂ : Set T}
[DecidablePred fun (x : T) => x ∈ U₁]
[DecidablePred fun (x : T) => x ∈ U₂]
(hU₁ : IsOpen U₁)
(hU₂ : IsOpen U₂)
{X₁ X₂ : T → Ω → E}
{c₁ c₂ : ENNReal}
{p₁ p₂ q₁ q₂ d₁ d₂ : ℝ}
{M₁ M₂ β₁ β₂ : NNReal}
(hT₁ : HasBoundedInternalCoveringNumber U₁ c₁ d₁)
(hT₂ : HasBoundedInternalCoveringNumber U₂ c₂ d₂)
(hX₁ : IsKolmogorovProcess X₁ P p₁ q₁ M₁)
(hX₂ : IsKolmogorovProcess X₂ P p₂ q₂ M₂)
(hc₁ : c₁ ≠ ⊤)
(hc₂ : c₂ ≠ ⊤)
(hd₁_pos : 0 < d₁)
(hd₂_pos : 0 < d₂)
(hdq₁_lt : d₁ < q₁)
(hdq₂_lt : d₂ < q₂)
(hβ₁_pos : 0 < β₁)
(hβ₂_pos : 0 < β₂)
(hβ₁_lt : ↑β₁ < (q₁ - d₁) / p₁)
(hβ₂_lt : ↑β₂ < (q₂ - d₂) / p₂)
(hX₁₂ : ∀ (i j : T), Measurable fun (ω : Ω) => (X₁ i ω, X₂ j ω))
(s t : T)
:
Measurable fun (ω : Ω) => (holderModification X₁ β₁ p₁ U₁ s ω, holderModification X₂ β₂ p₂ U₂ t ω)
theorem
ProbabilityTheory.measurable_pair_holderModification_self
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{X : T → Ω → E}
{c : ENNReal}
{d p q : ℝ}
{M β : NNReal}
{P : MeasureTheory.Measure Ω}
{U : Set T}
[PseudoEMetricSpace T]
[EMetricSpace E]
[hE : Nonempty E]
[MeasurableSpace E]
[BorelSpace E]
[CompleteSpace E]
[SecondCountableTopology T]
(hT : HasBoundedInternalCoveringNumber U c d)
[DecidablePred fun (x : T) => x ∈ U]
(hU : IsOpen U)
(hX : IsKolmogorovProcess X P p q M)
(hc : c ≠ ⊤)
(hd_pos : 0 < d)
(hdq_lt : d < q)
(hβ_pos : 0 < β)
(hβ_lt : ↑β < (q - d) / p)
(s t : T)
:
Measurable fun (ω : Ω) => (holderModification X β p U s ω, holderModification X β p U t ω)
theorem
ProbabilityTheory.measurable_edist_holderModification
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[PseudoEMetricSpace T]
[EMetricSpace E]
[hE : Nonempty E]
[MeasurableSpace E]
[BorelSpace E]
[CompleteSpace E]
[SecondCountableTopology T]
{U₁ U₂ : Set T}
[DecidablePred fun (x : T) => x ∈ U₁]
[DecidablePred fun (x : T) => x ∈ U₂]
(hU₁ : IsOpen U₁)
(hU₂ : IsOpen U₂)
{X₁ X₂ : T → Ω → E}
{c₁ c₂ : ENNReal}
{p₁ p₂ q₁ q₂ d₁ d₂ : ℝ}
{M₁ M₂ β₁ β₂ : NNReal}
(hT₁ : HasBoundedInternalCoveringNumber U₁ c₁ d₁)
(hT₂ : HasBoundedInternalCoveringNumber U₂ c₂ d₂)
(hX₁ : IsKolmogorovProcess X₁ P p₁ q₁ M₁)
(hX₂ : IsKolmogorovProcess X₂ P p₂ q₂ M₂)
(hc₁ : c₁ ≠ ⊤)
(hc₂ : c₂ ≠ ⊤)
(hd₁_pos : 0 < d₁)
(hd₂_pos : 0 < d₂)
(hdq₁_lt : d₁ < q₁)
(hdq₂_lt : d₂ < q₂)
(hβ₁_pos : 0 < β₁)
(hβ₂_pos : 0 < β₂)
(hβ₁_lt : ↑β₁ < (q₁ - d₁) / p₁)
(hβ₂_lt : ↑β₂ < (q₂ - d₂) / p₂)
(hX₁₂ : ∀ (i j : T), Measurable fun (ω : Ω) => (X₁ i ω, X₂ j ω))
(s t : T)
:
Measurable fun (ω : Ω) => edist (holderModification X₁ β₁ p₁ U₁ s ω) (holderModification X₂ β₂ p₂ U₂ t ω)
theorem
ProbabilityTheory.measurable_edist_holderModification'
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{X : T → Ω → E}
{c : ENNReal}
{d p q : ℝ}
{M : NNReal}
{P : MeasureTheory.Measure Ω}
{U : Set T}
[PseudoEMetricSpace T]
[EMetricSpace E]
[hE : Nonempty E]
[MeasurableSpace E]
[BorelSpace E]
[CompleteSpace E]
[SecondCountableTopology T]
{β₁ β₂ : NNReal}
(hT : HasBoundedInternalCoveringNumber U c d)
[DecidablePred fun (x : T) => x ∈ U]
(hU : IsOpen U)
(hX : IsKolmogorovProcess X P p q M)
(hc : c ≠ ⊤)
(hd_pos : 0 < d)
(hdq_lt : d < q)
(hβ₁_pos : 0 < β₁)
(hβ₁_lt : ↑β₁ < (q - d) / p)
(hβ₂_pos : 0 < β₂)
(hβ₂_lt : ↑β₂ < (q - d) / p)
(s t : T)
:
Measurable fun (ω : Ω) => edist (holderModification X β₁ p U s ω) (holderModification X β₂ p U t ω)
theorem
ProbabilityTheory.holderOnWith_holderModification
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{X : T → Ω → E}
{c : ENNReal}
{d p q : ℝ}
{M β : NNReal}
{P : MeasureTheory.Measure Ω}
{U : Set T}
[PseudoEMetricSpace T]
[EMetricSpace E]
[hE : Nonempty E]
[CompleteSpace E]
[SecondCountableTopology T]
(hT : HasBoundedInternalCoveringNumber U c d)
[DecidablePred fun (x : T) => x ∈ U]
(hU : IsOpen U)
(hX : IsKolmogorovProcess X P p q M)
(hd_pos : 0 < d)
(hβ_pos : 0 < β)
(ω : Ω)
:
∃ (C : NNReal), HolderOnWith C β (fun (x : T) => holderModification X β p U x ω) U
theorem
ProbabilityTheory.uniformContinuousOn_holderModification
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{X : T → Ω → E}
{c : ENNReal}
{d p q : ℝ}
{M β : NNReal}
{P : MeasureTheory.Measure Ω}
{U : Set T}
[PseudoEMetricSpace T]
[EMetricSpace E]
[hE : Nonempty E]
[CompleteSpace E]
[SecondCountableTopology T]
(hT : HasBoundedInternalCoveringNumber U c d)
[DecidablePred fun (x : T) => x ∈ U]
(hU : IsOpen U)
(hX : IsKolmogorovProcess X P p q M)
(hd_pos : 0 < d)
(hβ_pos : 0 < β)
(ω : Ω)
:
UniformContinuousOn (fun (t : T) => holderModification X β p U t ω) U
theorem
ProbabilityTheory.continuousOn_holderModification
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{X : T → Ω → E}
{c : ENNReal}
{d p q : ℝ}
{M β : NNReal}
{P : MeasureTheory.Measure Ω}
{U : Set T}
[PseudoEMetricSpace T]
[EMetricSpace E]
[hE : Nonempty E]
[CompleteSpace E]
[SecondCountableTopology T]
(hT : HasBoundedInternalCoveringNumber U c d)
[DecidablePred fun (x : T) => x ∈ U]
(hU : IsOpen U)
(hX : IsKolmogorovProcess X P p q M)
(hd_pos : 0 < d)
(hβ_pos : 0 < β)
(ω : Ω)
:
ContinuousOn (fun (t : T) => holderModification X β p U t ω) U
theorem
ProbabilityTheory.modification_holderModification
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{X : T → Ω → E}
{c : ENNReal}
{d p q : ℝ}
{M β : NNReal}
{P : MeasureTheory.Measure Ω}
{U : Set T}
[PseudoEMetricSpace T]
[EMetricSpace E]
[hE : Nonempty E]
[MeasurableSpace E]
[BorelSpace E]
[CompleteSpace E]
[SecondCountableTopology T]
[MeasureTheory.IsFiniteMeasure P]
(hT : HasBoundedInternalCoveringNumber U c d)
[DecidablePred fun (x : T) => x ∈ U]
(hU : IsOpen U)
(hX : IsKolmogorovProcess X P p q M)
(hc : c ≠ ⊤)
(hd_pos : 0 < d)
(hdq_lt : d < q)
(hβ_pos : 0 < β)
(hβ_lt : ↑β < (q - d) / p)
(t : T)
(htU : t ∈ U)
:
theorem
ProbabilityTheory.exists_modification_holder_aux'
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{X : T → Ω → E}
{c : ENNReal}
{d p q : ℝ}
{M β : NNReal}
{P : MeasureTheory.Measure Ω}
{U : Set T}
[PseudoEMetricSpace T]
[EMetricSpace E]
[hE : Nonempty E]
[MeasurableSpace E]
[BorelSpace E]
[CompleteSpace E]
[SecondCountableTopology T]
[MeasureTheory.IsFiniteMeasure P]
(hT : HasBoundedInternalCoveringNumber U c d)
[DecidablePred fun (x : T) => x ∈ U]
(hU : IsOpen U)
(hX : IsKolmogorovProcess X P p q M)
(hc : c ≠ ⊤)
(hd_pos : 0 < d)
(hdq_lt : d < q)
(hβ_pos : 0 < β)
(hβ_lt : ↑β < (q - d) / p)
:
∃ (Y : T → Ω → E),
(∀ (t : T), Measurable (Y t)) ∧ (∀ t ∈ U, Y t =ᵐ[P] X t) ∧ (∀ (ω : Ω), ∃ (C : NNReal), HolderOnWith C β (fun (x : T) => Y x ω) U) ∧ IsLimitOfIndicator Y X P U
theorem
ProbabilityTheory.exists_modification_holder_aux
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{X : T → Ω → E}
{c : ENNReal}
{d p q : ℝ}
{M β : NNReal}
{P : MeasureTheory.Measure Ω}
{U : Set T}
[PseudoEMetricSpace T]
[EMetricSpace E]
[hE : Nonempty E]
[MeasurableSpace E]
[BorelSpace E]
[CompleteSpace E]
[SecondCountableTopology T]
[MeasureTheory.IsFiniteMeasure P]
(hT : HasBoundedInternalCoveringNumber U c d)
[DecidablePred fun (x : T) => x ∈ U]
(hU : IsOpen U)
(hX : IsAEKolmogorovProcess X P p q M)
(hc : c ≠ ⊤)
(hd_pos : 0 < d)
(hdq_lt : d < q)
(hβ_pos : 0 < β)
(hβ_lt : ↑β < (q - d) / p)
:
∃ (Y : T → Ω → E),
(∀ (t : T), Measurable (Y t)) ∧ (∀ t ∈ U, Y t =ᵐ[P] X t) ∧ ∀ (ω : Ω), ∃ (C : NNReal), HolderOnWith C β (fun (x : T) => Y x ω) U
theorem
ProbabilityTheory.StronglyMeasurable.measurableSet_eq_of_continuous
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace T]
[EMetricSpace E]
[SecondCountableTopology T]
{f g : T → Ω → E}
(hf : ∀ (ω : Ω), Continuous fun (x : T) => f x ω)
(hg : ∀ (ω : Ω), Continuous fun (x : T) => g x ω)
(hf_meas : ∀ (t : T), MeasureTheory.StronglyMeasurable (f t))
(hg_meas : ∀ (t : T), MeasureTheory.StronglyMeasurable (g t))
:
theorem
ProbabilityTheory.Measurable.measurableSet_eq_of_continuous
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace T]
[EMetricSpace E]
[SecondCountableTopology T]
{f g : T → Ω → E}
(hf : ∀ (ω : Ω), Continuous fun (x : T) => f x ω)
(hg : ∀ (ω : Ω), Continuous fun (x : T) => g x ω)
(h_meas : ∀ (t : T), Measurable fun (ω : Ω) => edist (f t ω) (g t ω))
:
theorem
ProbabilityTheory.Measurable.measurableSet_eqOn_of_continuous
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{U : Set T}
[PseudoEMetricSpace T]
[EMetricSpace E]
[SecondCountableTopology T]
{f g : T → Ω → E}
(hU : IsOpen U)
(hf : ∀ (ω : Ω), ContinuousOn (fun (x : T) => f x ω) U)
(hg : ∀ (ω : Ω), ContinuousOn (fun (x : T) => g x ω) U)
(h_meas : ∀ (t : T), Measurable fun (ω : Ω) => edist (f t ω) (g t ω))
:
theorem
ProbabilityTheory.exists_modification_holder''
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{X : T → Ω → E}
{c : ENNReal}
{d p q : ℝ}
{M : NNReal}
{P : MeasureTheory.Measure Ω}
{U : Set T}
[PseudoEMetricSpace T]
[EMetricSpace E]
[hE : Nonempty E]
[MeasurableSpace E]
[BorelSpace E]
[CompleteSpace E]
[SecondCountableTopology T]
[MeasureTheory.IsFiniteMeasure P]
(hT : HasBoundedInternalCoveringNumber U c d)
[DecidablePred fun (x : T) => x ∈ U]
(hU : IsOpen U)
(hX : IsKolmogorovProcess X P p q M)
(hc : c ≠ ⊤)
(hd_pos : 0 < d)
(hdq_lt : d < q)
:
∃ (Y : T → Ω → E),
(∀ (t : T), Measurable (Y t)) ∧ (∀ t ∈ U, Y t =ᵐ[P] X t) ∧ (∀ (β : NNReal),
0 < β → ↑β < (q - d) / p → ∀ (ω : Ω), ∃ (C : NNReal), HolderOnWith C β (fun (x : T) => Y x ω) U) ∧ IsLimitOfIndicator Y X P U
theorem
ProbabilityTheory.exists_modification_holder
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{X : T → Ω → E}
{c : ENNReal}
{d p q : ℝ}
{M : NNReal}
{P : MeasureTheory.Measure Ω}
{U : Set T}
[PseudoEMetricSpace T]
[EMetricSpace E]
[hE : Nonempty E]
[MeasurableSpace E]
[BorelSpace E]
[CompleteSpace E]
[SecondCountableTopology T]
[MeasureTheory.IsFiniteMeasure P]
(hT : HasBoundedInternalCoveringNumber U c d)
[DecidablePred fun (x : T) => x ∈ U]
(hU : IsOpen U)
(hX : IsAEKolmogorovProcess X P p q M)
(hc : c ≠ ⊤)
(hd_pos : 0 < d)
(hdq_lt : d < q)
:
theorem
IsCoverWithBoundedCoveringNumber.hasBoundedInternalCoveringNumber_univ
{T : Type u_1}
{d : ℝ}
[PseudoEMetricSpace T]
{C : ℕ → Set T}
{c : ℕ → ENNReal}
(hC : IsCoverWithBoundedCoveringNumber C Set.univ c fun (x : ℕ) => d)
(n : ℕ)
:
theorem
ProbabilityTheory.exists_modification_holder'''
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{X : T → Ω → E}
{d p q : ℝ}
{M : NNReal}
{P : MeasureTheory.Measure Ω}
[PseudoEMetricSpace T]
[EMetricSpace E]
[hE : Nonempty E]
[MeasurableSpace E]
[BorelSpace E]
[CompleteSpace E]
[SecondCountableTopology T]
[MeasureTheory.IsFiniteMeasure P]
{C : ℕ → Set T}
{c : ℕ → ENNReal}
(hC : IsCoverWithBoundedCoveringNumber C Set.univ c fun (x : ℕ) => d)
(hX : IsKolmogorovProcess X P p q M)
(hc : ∀ (n : ℕ), c n ≠ ⊤)
(hd_pos : 0 < d)
(hdq_lt : d < q)
:
theorem
ProbabilityTheory.exists_modification_holder'
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{X : T → Ω → E}
{d p q : ℝ}
{M : NNReal}
{P : MeasureTheory.Measure Ω}
[PseudoEMetricSpace T]
[EMetricSpace E]
[hE : Nonempty E]
[MeasurableSpace E]
[BorelSpace E]
[CompleteSpace E]
[SecondCountableTopology T]
[MeasureTheory.IsFiniteMeasure P]
{C : ℕ → Set T}
{c : ℕ → ENNReal}
(hC : IsCoverWithBoundedCoveringNumber C Set.univ c fun (x : ℕ) => d)
(hX : IsAEKolmogorovProcess X P p q M)
(hc : ∀ (n : ℕ), c n ≠ ⊤)
(hd_pos : 0 < d)
(hdq_lt : d < q)
:
theorem
ProbabilityTheory.exists_modification_holder_iSup'
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{X : T → Ω → E}
{d : ℝ}
{P : MeasureTheory.Measure Ω}
[PseudoEMetricSpace T]
[EMetricSpace E]
[hE : Nonempty E]
[MeasurableSpace E]
[BorelSpace E]
[CompleteSpace E]
[SecondCountableTopology T]
[MeasureTheory.IsFiniteMeasure P]
{C : ℕ → Set T}
{c : ℕ → ENNReal}
{p q : ℕ → ℝ}
{M : ℕ → NNReal}
(hC : IsCoverWithBoundedCoveringNumber C Set.univ c fun (x : ℕ) => d)
(hX : ∀ (n : ℕ), IsKolmogorovProcess X P (p n) (q n) (M n))
(hc : ∀ (n : ℕ), c n ≠ ⊤)
(hd_pos : 0 < d)
(hdq_lt : ∀ (n : ℕ), d < q n)
:
theorem
ProbabilityTheory.exists_modification_holder_iSup
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{X : T → Ω → E}
{d : ℝ}
{P : MeasureTheory.Measure Ω}
[PseudoEMetricSpace T]
[EMetricSpace E]
[hE : Nonempty E]
[MeasurableSpace E]
[BorelSpace E]
[CompleteSpace E]
[SecondCountableTopology T]
[MeasureTheory.IsFiniteMeasure P]
{C : ℕ → Set T}
{c : ℕ → ENNReal}
{p q : ℕ → ℝ}
{M : ℕ → NNReal}
(hC : IsCoverWithBoundedCoveringNumber C Set.univ c fun (x : ℕ) => d)
(hX : ∀ (n : ℕ), IsAEKolmogorovProcess X P (p n) (q n) (M n))
(hc : ∀ (n : ℕ), c n ≠ ⊤)
(hd_pos : 0 < d)
(hdq_lt : ∀ (n : ℕ), d < q n)
: