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
exists_modification_of_edist_modification
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[PseudoEMetricSpace E]
[MeasurableSpace E]
[BorelSpace E]
{X Y : T → Ω → E}
(hY : ∀ (t : T), Measurable (Y t))
(h_edist : ∀ (t : T), ∀ᵐ (ω : Ω) ∂P, edist (Y t ω) (X t ω) = 0)
:
∃ (Z : T → Ω → E),
(∀ (t : T), Measurable (Z t)) ∧ (∀ (t : T) (ω : Ω), edist (Z t ω) (Y t ω) = 0) ∧ ∀ (t : T), Z t =ᵐ[P] X t
theorem
exists_modification_on_of_edist_modification_on
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[PseudoEMetricSpace E]
[MeasurableSpace E]
[BorelSpace E]
{X Y : T → Ω → E}
(hY : ∀ (t : T), Measurable (Y t))
{U : Set T}
(h_edist : ∀ t ∈ U, ∀ᵐ (ω : Ω) ∂P, edist (Y t ω) (X t ω) = 0)
:
∃ (Z : T → Ω → E),
(∀ (t : T), Measurable (Z t)) ∧ (∀ (t : T) (ω : Ω), edist (Z t ω) (Y t ω) = 0) ∧ ∀ t ∈ U, Z t =ᵐ[P] X t
theorem
IsCoverWithBoundedCoveringNumber.HasBoundedCoveringNumber_univ
{T : Type u_1}
{d : ℝ}
[PseudoEMetricSpace T]
{C : ℕ → Set T}
{c : ℕ → ENNReal}
(hC : IsCoverWithBoundedCoveringNumber C Set.univ c fun (x : ℕ) => d)
(n : ℕ)
:
Metric.HasCoveringExponent Set.univ (c n) d
theorem
Measurable.measurableSet_edist_eq_zero_of_continuous
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace T]
[PseudoEMetricSpace 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.edist (f t ω) (g t ω))
:
MeasurableSet {ω : Ω | ∀ (t : T), EDist.edist (f t ω) (g t ω) = 0}
theorem
Measurable.measurableSet_edist_eqOn_zero_of_continuous
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{U : Set T}
[PseudoEMetricSpace T]
[PseudoEMetricSpace 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.edist (f t ω) (g t ω))
:
MeasurableSet {ω : Ω | ∀ t ∈ U, EDist.edist (f t ω) (g t ω) = 0}
def
ProbabilityTheory.holderSet
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[PseudoEMetricSpace T]
[PseudoEMetricSpace 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]
[PseudoEMetricSpace 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]
[PseudoEMetricSpace E]
(hT : Metric.HasCoveringExponent U c 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]
[PseudoEMetricSpace E]
(hT : Metric.HasCoveringExponent U c 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]
[PseudoEMetricSpace E]
(hT : Metric.HasCoveringExponent U c 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]
[PseudoEMetricSpace E]
[CompleteSpace E]
(hT : Metric.HasCoveringExponent U c d)
(hU : IsOpen U)
(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]
[PseudoEMetricSpace E]
[MeasurableSpace E]
[BorelSpace E]
(hT : Metric.HasCoveringExponent 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]
[PseudoEMetricSpace 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)
noncomputable def
ProbabilityTheory.holderModification
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[PseudoEMetricSpace T]
[PseudoEMetricSpace 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]
[PseudoEMetricSpace E]
[MeasurableSpace E]
[BorelSpace E]
[CompleteSpace E]
[hE : Nonempty E]
[SecondCountableTopology T]
(hT : Metric.HasCoveringExponent 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.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]
[PseudoEMetricSpace E]
[CompleteSpace E]
[hE : Nonempty E]
(hT : Metric.HasCoveringExponent U c d)
(hU : IsOpen U)
(hX : IsKolmogorovProcess X P p q M)
(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]
[PseudoEMetricSpace E]
[MeasurableSpace E]
[BorelSpace E]
[CompleteSpace E]
[hE : Nonempty E]
[SecondCountableTopology T]
(hT : Metric.HasCoveringExponent 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.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]
[PseudoEMetricSpace E]
[CompleteSpace E]
[hE : Nonempty E]
[SecondCountableTopology T]
(hT : Metric.HasCoveringExponent U c d)
[DecidablePred fun (x : T) => x ∈ U]
(hU : IsOpen U)
(hX : IsKolmogorovProcess X P p q M)
(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]
[PseudoEMetricSpace E]
[CompleteSpace E]
[hE : Nonempty E]
[SecondCountableTopology T]
(hT : Metric.HasCoveringExponent U c d)
[DecidablePred fun (x : T) => x ∈ U]
(hU : IsOpen U)
(hX : IsKolmogorovProcess X P p q M)
(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]
[PseudoEMetricSpace E]
[CompleteSpace E]
[hE : Nonempty E]
[SecondCountableTopology T]
(hT : Metric.HasCoveringExponent U c d)
[DecidablePred fun (x : T) => x ∈ U]
(hU : IsOpen U)
(hX : IsKolmogorovProcess X P p q M)
(hβ_pos : 0 < β)
(ω : Ω)
:
ContinuousOn (fun (t : T) => holderModification X β p U t ω) U
theorem
ProbabilityTheory.measurable_pair_holderModification
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[PseudoEMetricSpace T]
[PseudoEMetricSpace E]
[MeasurableSpace E]
[BorelSpace E]
[CompleteSpace E]
[hE : Nonempty 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₁ : Metric.HasCoveringExponent U₁ c₁ d₁)
(hT₂ : Metric.HasCoveringExponent 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]
[PseudoEMetricSpace E]
[MeasurableSpace E]
[BorelSpace E]
[CompleteSpace E]
[hE : Nonempty E]
[SecondCountableTopology T]
(hT : Metric.HasCoveringExponent 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]
[PseudoEMetricSpace E]
[MeasurableSpace E]
[BorelSpace E]
[CompleteSpace E]
[hE : Nonempty 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₁ : Metric.HasCoveringExponent U₁ c₁ d₁)
(hT₂ : Metric.HasCoveringExponent 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]
[PseudoEMetricSpace E]
[MeasurableSpace E]
[BorelSpace E]
[CompleteSpace E]
[hE : Nonempty E]
[SecondCountableTopology T]
{β₁ β₂ : NNReal}
(hT : Metric.HasCoveringExponent 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.edist_holderModification_eq_zero
{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]
[PseudoEMetricSpace E]
[hE : Nonempty E]
[SecondCountableTopology T]
(hT : Metric.HasCoveringExponent U c d)
(hU : IsOpen U)
[DecidablePred fun (x : T) => x ∈ U]
(hX : IsKolmogorovProcess X P p q M)
(hβ_pos : 0 < β)
(t' : ↑(denseCountable T))
(ht'U : ↑t' ∈ U)
{ω : Ω}
(hω : ω ∈ holderSet X (denseCountable T) p (↑β) U)
:
theorem
ProbabilityTheory.edist_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]
[PseudoEMetricSpace E]
[MeasurableSpace E]
[BorelSpace E]
[CompleteSpace E]
[hE : Nonempty E]
[SecondCountableTopology T]
[MeasureTheory.IsFiniteMeasure P]
(hT : Metric.HasCoveringExponent 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_edist_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]
[PseudoEMetricSpace E]
[MeasurableSpace E]
[BorelSpace E]
[CompleteSpace E]
[hE : Nonempty E]
[SecondCountableTopology T]
[MeasureTheory.IsFiniteMeasure P]
(hT : Metric.HasCoveringExponent U c d)
(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, ∀ᵐ (ω : Ω) ∂P, edist (Y t ω) (X t ω) = 0) ∧ (∀ (ω : Ω), ∃ (C : NNReal), HolderOnWith C β (fun (x : T) => Y x ω) U) ∧ IsLimitOfIndicator Y X P U
theorem
HolderOnWith.congr_edist
{T : Type u_4}
{E : Type u_5}
[PseudoEMetricSpace T]
[PseudoEMetricSpace E]
{f g : T → E}
{U : Set T}
{C β : NNReal}
(hfg : ∀ (s t : T), s ∈ U → t ∈ U → edist (g s) (g t) = edist (f s) (f t))
(hf : HolderOnWith C β f U)
:
HolderOnWith C β g 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]
[PseudoEMetricSpace E]
[MeasurableSpace E]
[BorelSpace E]
[CompleteSpace E]
[hE : Nonempty E]
[SecondCountableTopology T]
[MeasureTheory.IsFiniteMeasure P]
(hT : Metric.HasCoveringExponent U c d)
(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]
[PseudoEMetricSpace E]
[MeasurableSpace E]
[BorelSpace E]
[CompleteSpace E]
[hE : Nonempty E]
[SecondCountableTopology T]
[MeasureTheory.IsFiniteMeasure P]
(hT : Metric.HasCoveringExponent U c d)
(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.indistinguishable_of_edist_modification_on
{T : Type u_4}
{Ω : Type u_5}
{E : Type u_6}
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace E]
[TopologicalSpace T]
[TopologicalSpace.SeparableSpace T]
{P : MeasureTheory.Measure Ω}
{U : Set T}
(hU : IsOpen U)
{X Y : T → Ω → E}
(hX : ∀ᵐ (ω : Ω) ∂P, ContinuousOn (fun (x : T) => X x ω) U)
(hY : ∀ᵐ (ω : Ω) ∂P, ContinuousOn (fun (x : T) => Y x ω) U)
(h : ∀ t ∈ U, ∀ᵐ (ω : Ω) ∂P, edist (X t ω) (Y t ω) = 0)
:
theorem
ProbabilityTheory.indistinguishable_of_edist_modification
{T : Type u_4}
{Ω : Type u_5}
{E : Type u_6}
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace E]
[TopologicalSpace T]
[TopologicalSpace.SeparableSpace T]
{P : MeasureTheory.Measure Ω}
{X Y : T → Ω → E}
(hX : ∀ᵐ (ω : Ω) ∂P, Continuous fun (x : T) => X x ω)
(hY : ∀ᵐ (ω : Ω) ∂P, Continuous fun (x : T) => Y x ω)
(h : ∀ (t : T), ∀ᵐ (ω : Ω) ∂P, edist (X t ω) (Y t ω) = 0)
:
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]
[PseudoEMetricSpace E]
[MeasurableSpace E]
[BorelSpace E]
[CompleteSpace E]
[hE : Nonempty E]
[SecondCountableTopology T]
[MeasureTheory.IsFiniteMeasure P]
(hT : Metric.HasCoveringExponent U c d)
(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]
[PseudoEMetricSpace E]
[MeasurableSpace E]
[BorelSpace E]
[CompleteSpace E]
[hE : Nonempty E]
[SecondCountableTopology T]
[MeasureTheory.IsFiniteMeasure P]
(hT : Metric.HasCoveringExponent U c d)
(hU : IsOpen U)
(hX : IsAEKolmogorovProcess 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
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]
[PseudoEMetricSpace E]
[MeasurableSpace E]
[BorelSpace E]
[CompleteSpace E]
[hE : Nonempty 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)
:
∃ (Y : T → Ω → E),
(∀ (t : T), Measurable (Y t)) ∧ (∀ (t : T), Y t =ᵐ[P] X t) ∧ (∀ (ω : Ω) (t : T),
∃ U ∈ nhds t,
∀ (β : NNReal), 0 < β → ↑β < (q - d) / p → ∃ (C : NNReal), HolderOnWith C β (fun (x : T) => Y x ω) U) ∧ IsLimitOfIndicator Y X P Set.univ
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]
[PseudoEMetricSpace E]
[MeasurableSpace E]
[BorelSpace E]
[CompleteSpace E]
[hE : Nonempty 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]
[PseudoEMetricSpace E]
[MeasurableSpace E]
[BorelSpace E]
[CompleteSpace E]
[hE : Nonempty 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]
[PseudoEMetricSpace E]
[MeasurableSpace E]
[BorelSpace E]
[CompleteSpace E]
[hE : Nonempty 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)
:
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 : Metric.HasCoveringExponent U c d)
(hU : IsOpen U)
[DecidablePred fun (x : T) => x ∈ U]
(hX : IsKolmogorovProcess X P p q M)
(hβ_pos : 0 < β)
(t' : ↑(denseCountable T))
(ht'U : ↑t' ∈ U)
{ω : Ω}
(hω : ω ∈ holderSet X (denseCountable T) p (↑β) 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 : Metric.HasCoveringExponent 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)
:
holderModification X β p U t =ᵐ[P] X t
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 ω))
: