Kolmogorov-Chentsov theorem #
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
Asymptotics.IsEquivalent.add_const_of_norm_tendsto_atTop
{α : Type u_1}
{β : Type u_2}
[NormedField β]
[LinearOrder β]
[IsStrictOrderedRing β]
{u v : α → β}
{l : Filter α}
{c : β}
(huv : IsEquivalent l u v)
(hv : Filter.Tendsto (norm ∘ v) l Filter.atTop)
:
IsEquivalent l (fun (x : α) => u x + c) v
theorem
Asymptotics.IsEquivalent.const_add_of_norm_tendsto_atTop
{α : Type u_1}
{β : Type u_2}
[NormedField β]
[LinearOrder β]
[IsStrictOrderedRing β]
{u v : α → β}
{l : Filter α}
{c : β}
(huv : IsEquivalent l u v)
(hv : Filter.Tendsto (norm ∘ v) l Filter.atTop)
:
IsEquivalent l (fun (x : α) => c + u x) v
theorem
Asymptotics.IsEquivalent.add_add_of_nonneg
{α : Type u_1}
{t u v w : α → ℝ}
(hu : 0 ≤ u)
(hw : 0 ≤ w)
{l : Filter α}
(htu : IsEquivalent l t u)
(hvw : IsEquivalent l v w)
:
IsEquivalent l (t + v) (u + w)
theorem
Asymptotics.IsEquivalent.rpow_of_nonneg
{α : Type u_1}
{t u : α → ℝ}
(hu : 0 ≤ u)
{l : Filter α}
(h : IsEquivalent l t u)
{r : ℝ}
:
IsEquivalent l (t ^ r) (u ^ r)
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 : IsAEKolmogorovProcess X P p q M)
(hβ : 0 < β)
{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 : IsAEKolmogorovProcess X P p q M)
(hd_pos : 0 < d)
(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 : IsAEKolmogorovProcess X P p q M)
(hd_pos : 0 < d)
(hdq_lt : d < q)
(hβ_pos : 0 < β)
(T' : Set T)
[Countable ↑T']
:
theorem
ProbabilityTheory.IsKolmogorovProcess.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 : 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' : 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.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 Ω}
[PseudoMetricSpace T]
[EMetricSpace E]
(hX : IsKolmogorovProcess 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.IsKolmogorovProcess.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 : 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.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)
(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 : IsAEKolmogorovProcess X P p q M)
(hc : c ≠ ⊤)
(hd_pos : 0 < d)
(hdq_lt : d < q)
(hβ_pos : 0 < β)
(hβ_lt : ↑β < (q - d) / p)
:
theorem
ProbabilityTheory.StronglyMeasurable.measurableSet_eq_of_continuous
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
[PseudoMetricSpace 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.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 : IsAEKolmogorovProcess X P p q M)
(hc : c ≠ ⊤)
(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 Ω}
[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 : 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 Ω}
[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 : ℕ), IsAEKolmogorovProcess X P (p n) (q n) (M n))
(hc : ∀ (n : ℕ), c n ≠ ⊤)
(hd_pos : 0 < d)
(hdq_lt : ∀ (n : ℕ), d < q n)
: