Documentation

BrownianMotion.Continuity.KolmogorovChentsov

Kolmogorov-Chentsov theorem #

theorem tendstoInMeasure_of_tendsto_ae_of_stronglyMeasurable' {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [EMetricSpace E] {f : αE} {g : αE} [MeasureTheory.IsFiniteMeasure μ] (hf : ∀ (n : ), MeasureTheory.StronglyMeasurable (f n)) (hg : MeasureTheory.StronglyMeasurable g) (hfg : ∀ᵐ (x : α) μ, Filter.Tendsto (fun (n : ) => f n x) Filter.atTop (nhds (g x))) (ε : ENNReal) :
0 < εFilter.Tendsto (fun (i : ) => μ {x : α | ε edist (f i x) (g x)}) Filter.atTop (nhds 0)
theorem lintegral_eq_zero_of_zero_ae {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : αENNReal} :
f =ᵐ[μ] 0∫⁻ (a : α), f a μ = 0
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 : ιXE} [hE : Nonempty E] (hf : ∀ (i : ι), Measurable (f i)) :
Measurable fun (x : X) => limUnder l fun (x_1 : ι) => f x_1 x
theorem MeasureTheory.Measure.measure_inter_eq_of_measure_eq_measure_univ {α : Type u_1} {x✝ : MeasurableSpace α} {μ : Measure α} {s t : Set α} (hs : MeasurableSet s) (h : μ t = μ Set.univ) (ht_ne_top : μ t ) :
μ (t s) = μ s
theorem MeasureTheory.Measure.measure_inter_eq_of_ae {α : Type u_1} {x✝ : MeasurableSpace α} {μ : Measure α} [IsFiniteMeasure μ] {s t : Set α} (hs : MeasurableSet s) (ht : NullMeasurableSet t μ) (h : ∀ᵐ (a : α) μ, a t) (ht_ne_top : μ t ) :
μ (t s) = μ s
theorem biSup_prod' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CompleteLattice α] {f : βγα} {s : Set β} {t : Set γ} :
xs ×ˢ t, f x.1 x.2 = as, bt, f a b
theorem Set.iUnion_le_nat :
⋃ (n : ), {i : | i n} = univ
structure FiniteExhaustion {α : Type u_1} (s : Set α) :
Type u_1
Instances For
    instance FiniteExhaustion.instFiniteElemCoeNatSet {α : Type u_1} {s : Set α} {K : FiniteExhaustion s} {n : } :
    Finite (K n)
    @[simp]
    theorem FiniteExhaustion.toFun_eq_coe {α : Type u_1} {s : Set α} (K : FiniteExhaustion s) :
    K.toFun = K
    theorem FiniteExhaustion.Finite {α : Type u_1} {s : Set α} (K : FiniteExhaustion s) (n : ) :
    (K n).Finite
    theorem FiniteExhaustion.subset_succ {α : Type u_1} {s : Set α} (K : FiniteExhaustion s) (n : ) :
    K n K (n + 1)
    theorem FiniteExhaustion.subset {α : Type u_1} {s : Set α} (K : FiniteExhaustion s) {m n : } (h : m n) :
    K m K n
    theorem FiniteExhaustion.iUnion_eq {α : Type u_1} {s : Set α} (K : FiniteExhaustion s) :
    ⋃ (n : ), K n = s
    noncomputable def FiniteExhaustion.choice {α : Type u_2} (s : Set α) [Countable s] :
    Equations
    Instances For
      def FiniteExhaustion.prod {α : Type u_1} {s : Set α} (K : FiniteExhaustion s) {β : Type u_2} {t : Set β} (K' : FiniteExhaustion t) :
      Equations
      • K.prod K' = { toFun := fun (n : ) => K n ×ˢ K' n, Finite' := , subset_succ' := , iUnion_eq' := }
      Instances For
        theorem FiniteExhaustion.prod_apply {α : Type u_1} {s : Set α} (K : FiniteExhaustion s) {β : Type u_2} {t : Set β} (K' : FiniteExhaustion t) (n : ) :
        (K.prod K') n = K n ×ˢ K' n
        theorem ProbabilityTheory.lintegral_div_edist_le_sum_integral_edist_le {T : Type u_1} {Ω : Type u_2} {E : Type u_3} { : MeasurableSpace Ω} {X : TΩE} {p q : } {M β : NNReal} {P : MeasureTheory.Measure Ω} [PseudoEMetricSpace T] [PseudoEMetricSpace E] [MeasurableSpace E] [BorelSpace E] (hT : EMetric.diam Set.univ < ) (hX : IsKolmogorovProcess X P p q M) ( : 0 < β) (hp : 0 < p) (hq : 0 < q) {J : Set T} [Countable J] :
        ∫⁻ (ω : Ω), ⨆ (s : J), ⨆ (t : J), edist (X (↑s) ω) (X (↑t) ω) ^ p / edist s t ^ (β * p) P ∑' (k : ), 2 ^ (k * β * p) * ∫⁻ (ω : Ω), ⨆ (s : J), ⨆ (t : { t : J // edist s t 2 * 2⁻¹ ^ k * (EMetric.diam Set.univ + 1) }), edist (X (↑s) ω) (X (↑t) ω) ^ p P
        noncomputable def ProbabilityTheory.constL (T : Type u_4) [PseudoEMetricSpace T] (c : ENNReal) (d p q β : ) :
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          theorem ProbabilityTheory.constL_lt_top {T : Type u_1} {c : ENNReal} {d p q : } {β : NNReal} [PseudoEMetricSpace T] (hc : c ) (hd_pos : 0 < d) (hp_pos : 0 < p) (hdq_lt : d < q) (hβ_pos : 0 < β) (hβ_lt : β < (q - d) / p) :
          constL T c d p q β <
          theorem ProbabilityTheory.finite_kolmogorov_chentsov {T : Type u_1} {Ω : Type u_2} {E : Type u_3} { : MeasurableSpace Ω} {X : TΩE} {c : ENNReal} {d p q : } {M β : NNReal} {P : MeasureTheory.Measure Ω} [PseudoEMetricSpace T] [PseudoEMetricSpace E] [MeasurableSpace E] [BorelSpace E] (hT : HasBoundedInternalCoveringNumber Set.univ c d) (hX : IsKolmogorovProcess X P p q M) (hd_pos : 0 < d) (hp_pos : 0 < p) (hdq_lt : d < q) (hβ_pos : 0 < β) (T' : Set T) [hT' : Finite T'] :
          ∫⁻ (ω : Ω), ⨆ (s : T'), ⨆ (t : T'), edist (X (↑s) ω) (X (↑t) ω) ^ p / edist s t ^ (β * p) P M * constL T c d p q β
          theorem ProbabilityTheory.countable_kolmogorov_chentsov {T : Type u_1} {Ω : Type u_2} {E : Type u_3} { : MeasurableSpace Ω} {X : TΩE} {c : ENNReal} {d p q : } {M β : NNReal} {P : MeasureTheory.Measure Ω} [PseudoEMetricSpace T] [PseudoEMetricSpace E] [MeasurableSpace E] [BorelSpace E] (hT : HasBoundedInternalCoveringNumber Set.univ c d) (hX : IsKolmogorovProcess X P p q M) (hd_pos : 0 < d) (hp_pos : 0 < p) (hdq_lt : d < q) (hβ_pos : 0 < β) (T' : Set T) [Countable T'] :
          ∫⁻ (ω : Ω), ⨆ (s : T'), ⨆ (t : T'), edist (X (↑s) ω) (X (↑t) ω) ^ p / edist s t ^ (β * p) P M * constL T c d p q β
          theorem ProbabilityTheory.IsMeasurableKolmogorovProcess.ae_iSup_rpow_edist_div_lt_top {T : Type u_1} {Ω : Type u_2} {E : Type u_3} { : MeasurableSpace Ω} {X : TΩE} {c : ENNReal} {d p q : } {M β : NNReal} {P : MeasureTheory.Measure Ω} [PseudoMetricSpace T] [EMetricSpace E] [MeasurableSpace E] [BorelSpace E] (hT : HasBoundedInternalCoveringNumber Set.univ c d) (hX : IsMeasurableKolmogorovProcess X P p q M) (hc : c ) (hd_pos : 0 < d) (hp_pos : 0 < p) (hdq_lt : d < q) (hβ_pos : 0 < β) (hβ_lt : β < (q - d) / p) {T' : Set T} (hT' : T'.Countable) :
          ∀ᵐ (ω : Ω) P, ⨆ (s : T'), ⨆ (t : T'), edist (X (↑s) ω) (X (↑t) ω) ^ p / edist s t ^ (β * p) <
          def ProbabilityTheory.holderSet {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [PseudoMetricSpace T] [EMetricSpace E] (X : TΩE) (T' : Set T) (p β : ) :
          Set Ω
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            theorem ProbabilityTheory.IsMeasurableKolmogorovProcess.measurableSet_holderSet {T : Type u_1} {Ω : Type u_2} {E : Type u_3} { : MeasurableSpace Ω} {X : TΩE} {p q : } {M β : NNReal} {P : MeasureTheory.Measure Ω} [PseudoMetricSpace T] [EMetricSpace E] (hX : IsMeasurableKolmogorovProcess X P p q M) {T' : Set T} (hT' : T'.Countable) :
            MeasurableSet (holderSet X T' p β)
            theorem ProbabilityTheory.holderWith_of_mem_holderSet {T : Type u_1} {Ω : Type u_2} {E : Type u_3} {X : TΩE} {c : ENNReal} {d p : } {β : NNReal} [PseudoMetricSpace T] [EMetricSpace E] (hT : HasBoundedInternalCoveringNumber Set.univ c d) (hd_pos : 0 < d) (hp_pos : 0 < p) (hβ_pos : 0 < β) {T' : Set T} {ω : Ω} ( : ω holderSet X T' p β) :
            HolderWith ((fun (ω : Ω) => ⨆ (s : T'), ⨆ (t : T'), edist (X (↑s) ω) (X (↑t) ω) ^ p / edist s t ^ (β * p)) ω ^ p⁻¹).toNNReal β fun (t : T') => X (↑t) ω
            theorem ProbabilityTheory.uniformContinuous_of_mem_holderSet {T : Type u_1} {Ω : Type u_2} {E : Type u_3} {X : TΩE} {c : ENNReal} {d p : } {β : NNReal} [PseudoMetricSpace T] [EMetricSpace E] (hT : HasBoundedInternalCoveringNumber Set.univ c d) (hd_pos : 0 < d) (hp_pos : 0 < p) (hβ_pos : 0 < β) {T' : Set T} {ω : Ω} ( : ω holderSet X T' p β) :
            UniformContinuous fun (t : T') => X (↑t) ω
            theorem ProbabilityTheory.continuous_of_mem_holderSet {T : Type u_1} {Ω : Type u_2} {E : Type u_3} {X : TΩE} {c : ENNReal} {d p : } {β : NNReal} [PseudoMetricSpace T] [EMetricSpace E] (hT : HasBoundedInternalCoveringNumber Set.univ c d) (hd_pos : 0 < d) (hp_pos : 0 < p) (hβ_pos : 0 < β) {T' : Set T} {ω : Ω} ( : ω holderSet X T' p β) :
            Continuous fun (t : T') => X (↑t) ω
            theorem ProbabilityTheory.IsMeasurableKolmogorovProcess.tendstoInMeasure_of_mem_holderSet {T : Type u_1} {Ω : Type u_2} {E : Type u_3} { : MeasurableSpace Ω} {X : TΩE} {p q : } {M : NNReal} {P : MeasureTheory.Measure Ω} [PseudoMetricSpace T] [EMetricSpace E] (hX : IsMeasurableKolmogorovProcess X P p q M) (hp_pos : 0 < p) (hq_pos : 0 < q) {T' : Set T} {u : T'} {t : T} (hu : Filter.Tendsto (fun (n : ) => (u n)) Filter.atTop (nhds t)) {ε : ENNReal} ( : 0 < ε) :
            Filter.Tendsto (fun (n : ) => P {ω : Ω | ε edist (X (↑(u n)) ω) (X t ω)}) Filter.atTop (nhds 0)
            theorem ProbabilityTheory.exists_modification_holder_aux' {T : Type u_1} {Ω : Type u_2} {E : Type u_3} { : MeasurableSpace Ω} {X : TΩE} {c : ENNReal} {d p q : } {M β : NNReal} {P : MeasureTheory.Measure Ω} [PseudoMetricSpace T] [EMetricSpace E] [MeasurableSpace E] [BorelSpace E] [Nonempty E] [SecondCountableTopology T] [CompleteSpace E] [SecondCountableTopology E] [MeasureTheory.IsFiniteMeasure P] (hT : HasBoundedInternalCoveringNumber Set.univ c d) (hX : IsMeasurableKolmogorovProcess X P p q M) (hc : c ) (hd_pos : 0 < d) (hp_pos : 0 < p) (hdq_lt : d < q) (hβ_pos : 0 < β) (hβ_lt : β < (q - d) / p) :
            ∃ (Y : TΩE), (∀ (t : T), Measurable (Y t)) (∀ (t : T), Y t =ᵐ[P] X t) ∀ (ω : Ω), ∃ (C : NNReal), HolderWith C β fun (x : T) => Y x ω
            theorem ProbabilityTheory.exists_modification_holder_aux {T : Type u_1} {Ω : Type u_2} {E : Type u_3} { : MeasurableSpace Ω} {X : TΩE} {c : ENNReal} {d p q : } {M β : NNReal} {P : MeasureTheory.Measure Ω} [PseudoMetricSpace T] [EMetricSpace E] [MeasurableSpace E] [BorelSpace E] [Nonempty E] [SecondCountableTopology T] [CompleteSpace E] [SecondCountableTopology E] [MeasureTheory.IsFiniteMeasure P] (hT : HasBoundedInternalCoveringNumber Set.univ c d) (hX : IsKolmogorovProcess X P p q M) (hc : c ) (hd_pos : 0 < d) (hp_pos : 0 < p) (hdq_lt : d < q) (hβ_pos : 0 < β) (hβ_lt : β < (q - d) / p) :
            ∃ (Y : TΩE), (∀ (t : T), Measurable (Y t)) (∀ (t : T), Y t =ᵐ[P] X t) ∀ (ω : Ω), MemHolder β fun (x : T) => Y x ω
            theorem ProbabilityTheory.exists_modification_holder {T : Type u_1} {Ω : Type u_2} {E : Type u_3} { : MeasurableSpace Ω} {X : TΩE} {c : ENNReal} {d p q : } {M : NNReal} {P : MeasureTheory.Measure Ω} [PseudoMetricSpace T] [EMetricSpace E] [MeasurableSpace E] [BorelSpace E] [Nonempty E] [SecondCountableTopology T] [CompleteSpace E] [SecondCountableTopology E] [MeasureTheory.IsFiniteMeasure P] (hT : HasBoundedInternalCoveringNumber Set.univ c d) (hX : IsKolmogorovProcess X P p q M) (hc : c ) (hd_pos : 0 < d) (hp_pos : 0 < p) (hdq_lt : d < q) :
            ∃ (Y : TΩE), (∀ (t : T), Measurable (Y t)) (∀ (t : T), Y t =ᵐ[P] X t) ∀ (β : NNReal), 0 < ββ < (q - d) / p∀ (ω : Ω), MemHolder β fun (x : T) => Y x ω
            theorem ProbabilityTheory.exists_modification_holder' {T : Type u_1} {Ω : Type u_2} {E : Type u_3} { : MeasurableSpace Ω} {X : TΩE} {d p q : } {M : NNReal} {P : MeasureTheory.Measure Ω} [PseudoMetricSpace T] [EMetricSpace E] [MeasurableSpace E] [BorelSpace E] [Nonempty E] [SecondCountableTopology T] [CompleteSpace E] [SecondCountableTopology E] [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 ) (hp_pos : 0 < p) (hdq_lt : d < q) :
            ∃ (Y : TΩE), (∀ (t : T), Measurable (Y t)) (∀ (t : T), Y t =ᵐ[P] X t) ∀ (β : NNReal), 0 < ββ < (q - d) / p∀ (ω : Ω), MemHolder β fun (x : T) => Y x ω
            theorem ProbabilityTheory.exists_modification_holder_iSup {T : Type u_1} {Ω : Type u_2} {E : Type u_3} { : MeasurableSpace Ω} {X : TΩE} {d : } {P : MeasureTheory.Measure Ω} [PseudoMetricSpace T] [EMetricSpace E] [MeasurableSpace E] [BorelSpace E] [Nonempty E] [SecondCountableTopology T] [CompleteSpace E] [SecondCountableTopology E] [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 ) (hp_pos : ∀ (n : ), 0 < p n) (hdq_lt : ∀ (n : ), d < q n) :
            ∃ (Y : TΩE), (∀ (t : T), Measurable (Y t)) (∀ (t : T), Y t =ᵐ[P] X t) ∀ (β : NNReal), 0 < ββ < ⨆ (n : ), (q n - d) / p n∀ (ω : Ω), MemHolder β fun (x : T) => Y x ω