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)
:
theorem
lintegral_eq_zero_of_zero_ae
{α : Type u_1}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{f : α → ENNReal}
:
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
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 ≠ ⊤)
:
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 ≠ ⊤)
:
theorem
biSup_prod'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[CompleteLattice α]
{f : β → γ → α}
{s : Set β}
{t : Set γ}
:
instance
FiniteExhaustion.instFunLikeNatSet
{α : Type u_1}
{s : Set α}
:
FunLike (FiniteExhaustion s) ℕ (Set α)
Equations
- FiniteExhaustion.instFunLikeNatSet = { coe := FiniteExhaustion.toFun, coe_injective' := ⋯ }
instance
FiniteExhaustion.instFiniteElemCoeNatSet
{α : Type u_1}
{s : Set α}
{K : FiniteExhaustion s}
{n : ℕ}
:
Finite ↑(K n)
@[simp]
theorem
FiniteExhaustion.Finite
{α : Type u_1}
{s : Set α}
(K : FiniteExhaustion s)
(n : ℕ)
:
(K n).Finite
theorem
FiniteExhaustion.subset
{α : Type u_1}
{s : Set α}
(K : FiniteExhaustion s)
{m n : ℕ}
(h : m ≤ n)
:
Equations
Instances For
def
FiniteExhaustion.prod
{α : Type u_1}
{s : Set α}
(K : FiniteExhaustion s)
{β : Type u_2}
{t : Set β}
(K' : FiniteExhaustion t)
:
FiniteExhaustion (s ×ˢ t)
Equations
Instances For
theorem
FiniteExhaustion.prod_apply
{α : Type u_1}
{s : Set α}
(K : FiniteExhaustion s)
{β : Type u_2}
{t : Set β}
(K' : FiniteExhaustion t)
(n : ℕ)
:
theorem
ProbabilityTheory.lintegral_div_edist_le_sum_integral_edist_le
{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]
[MeasurableSpace E]
[BorelSpace E]
(hT : EMetric.diam Set.univ < ⊤)
(hX : IsKolmogorovProcess X P p q M)
(hβ : 0 < β)
(hp : 0 < p)
(hq : 0 < q)
{J : Set T}
[Countable ↑J]
:
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.finite_kolmogorov_chentsov
{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 Ω}
[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']
:
theorem
ProbabilityTheory.countable_kolmogorov_chentsov
{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 Ω}
[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']
:
theorem
ProbabilityTheory.IsMeasurableKolmogorovProcess.ae_iSup_rpow_edist_div_lt_top
{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 Ω}
[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)
:
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}
{mΩ : 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}
{ω : Ω}
(hω : ω ∈ holderSet X T' p ↑β)
:
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}
{ω : Ω}
(hω : ω ∈ 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}
{ω : Ω}
(hω : ω ∈ 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}
{mΩ : 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}
(hε : 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}
{mΩ : 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}
{mΩ : 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)
:
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 Ω}
[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)
:
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 Ω}
[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)
:
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 Ω}
[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)
: