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.

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) : HolderOnWith ((fun (ω : Ω) => ⨆ (s : ↑(T' ∩ U)), ⨆ (t : ↑(T' ∩ U)), edist (X (↑s) ω) (X (↑t) ω) ^ p / edist s t ^ (↑β * p)) ω ^ p⁻¹).toNNReal β (fun (t : ↑T') => X (↑t) ω) {t' : ↑T' | ↑t' ∈ 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) : UniformContinuousOn (fun (t : ↑T') => X (↑t) ω) {x : ↑T' | ↑x ∈ 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) : ContinuousOn (fun (t : ↑T') => X (↑t) ω) {x : ↑T' | ↑x ∈ 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) : ∀ᵐ (ω : Ω) ∂P, ω ∈ holderSet X T' p (↑β) U

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.

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) : edist (holderModification X β p U (↑t') ω) (X (↑t') ω) = 0

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) : ∀ᵐ (ω : Ω) ∂P, edist (holderModification X β p U t ω) (X t ω) = 0

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) : ∀ᵐ (ω : Ω) ∂P, ∀ t ∈ U, 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) : ∀ᵐ (ω : Ω) ∂P, ∀ (t : T), 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) : ∃ (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

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) : ∃ (Y : T → Ω → E), (∀ (t : T), Measurable (Y t)) ∧ (∀ (t : T), Y t =ᵐ[P] X t) ∧ ∀ (ω : Ω) (t : T) (β : NNReal), 0 < β → ↑β < ⨆ (n : ℕ), (q n - d) / p n → ∃ U ∈ nhds t, ∃ (C : NNReal), HolderOnWith C β (fun (x : T) => Y x ω) U

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) : ∃ (Y : T → Ω → E), (∀ (t : T), Measurable (Y t)) ∧ (∀ (t : T), Y t =ᵐ[P] X t) ∧ ∀ (ω : Ω) (t : T) (β : NNReal), 0 < β → ↑β < ⨆ (n : ℕ), (q n - d) / p n → ∃ U ∈ nhds t, ∃ (C : NNReal), HolderOnWith C β (fun (x : T) => Y x ω) 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 : 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) : holderModification X β p U (↑t') ω = X (↑t') ω

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)) : MeasurableSet {ω : Ω | ∀ (t : T), f t ω = 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 ω)) : MeasurableSet {ω : Ω | ∀ (t : T), 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 ω)) : MeasurableSet {ω : Ω | ∀ t ∈ U, f t ω = g t ω}