Measure

Results named in Tau Ceti's TauCeti.MeasureTheory.Measure modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremHelly–Bray theorem#

Along a countably generated filter, probability measures on ℝ converge weakly if and only if their cumulative distribution functions converge pointwise at every continuity point of the limiting cumulative distribution function.

MeasureTheory.ProbabilityMeasure.tendsto_iff_forall_continuousAt_tendsto_cdf.{u_1} {ι : Type u_1}
  {l : Filter ι} {μs : ι → MeasureTheory.ProbabilityMeasure ℝ}
  {μ : MeasureTheory.ProbabilityMeasure ℝ} [l.IsCountablyGenerated] :
  Filter.Tendsto μs l (nhds μ) ↔
    ∀ (x : ℝ),
      ContinuousAt (↑(ProbabilityTheory.cdf ↑μ)) x →
        Filter.Tendsto (fun i => ↑(ProbabilityTheory.cdf ↑(μs i)) x) l
          (nhds (↑(ProbabilityTheory.cdf ↑μ) x))
Lean

Formalized in Tau Ceti as MeasureTheory.ProbabilityMeasure.tendsto_iff_forall_continuousAt_tendsto_cdf.

Sources
LeanMeasureTheory.ProbabilityMeasure.tendsto_iff_forall_continuousAt_tendsto_cdf

TheoremHölder–Markov estimate#

Let P be a measure on C([a, b], X) concentrated on curves absolutely continuous on [a, b], and 1 ≤ p. For η > 0 and every δ, the curves with two times closer than δ at which their values are at least η apart have P-measure at most δ ^ (p - 1) * (∫ A_p dP) / η ^ p, where A_p is the p-action over [a, b].

TauCeti.measure_continuity_modulus_le_lintegral_curveAction.{u_1} {X : Type u_1}
  [PseudoMetricSpace X] {a b p : ℝ} (hab : a ≤ b) {P : MeasureTheory.Measure C(↑(Set.Icc a b), X)}
  (hp : 1 ≤ p)
  (hAC :
    ∀ᵐ (γ : C(↑(Set.Icc a b), X)) ∂P, AbsolutelyContinuousOnInterval (Set.IccExtend hab ⇑γ) a b)
  {η : ℝ} (hη : 0 < η) (δ : ℝ) :
  P {γ | ∃ s t, dist s t < δ ∧ η ≤ dist (γ s) (γ t)} ≤
    (ENNReal.ofReal δ ^ (p - 1) *
        ∫⁻ (γ : C(↑(Set.Icc a b), X)), TauCeti.curveAction p (Set.IccExtend hab ⇑γ) a b ∂P) /
      ENNReal.ofReal η ^ p
Lean

Formalized in Tau Ceti as TauCeti.measure_continuity_modulus_le_lintegral_curveAction.

Sources
LeanTauCeti.measure_continuity_modulus_le_lintegral_curveAction
Uses 1 · Used by 1
Proof usesHölder estimate along a curve
Used byLisini's superposition principle in a complete separable metric space

TheoremLebesgue's differentiation theorem along dyadic cubes#

for an integrable g, at almost every x the averages of g over the dyadic cubes containing x converge to g x as the level tends to -∞.

TauCeti.ae_tendsto_setLAverage_dyadicCube.{u_1} {ι : Type u_1} [Fintype ι] {g : (ι → ℝ) → ENNReal}
  (hg : AEMeasurable g MeasureTheory.volume) (hg' : ∫⁻ (x : ι → ℝ), g x ≠ ⊤) :
  ∀ᵐ (x : ι → ℝ),
    Filter.Tendsto (fun k => ⨍⁻ (y : ι → ℝ) in TauCeti.dyadicCube k (TauCeti.dyadicIndex k x), g y)
      Filter.atBot (nhds (g x))
Lean

Formalized in Tau Ceti as TauCeti.ae_tendsto_setLAverage_dyadicCube.

Sources
LeanTauCeti.ae_tendsto_setLAverage_dyadicCube
Used by 4
Used byThe Calderón–Zygmund theorem · The dyadic John–Nirenberg inequality for any additive Haar measure · The Fefferman–Stein inequality · The John–Nirenberg inequality on Euclidean balls

TheoremLévy's continuity theorem, including existence#

If the characteristic functions of a sequence of probability measures converge pointwise to a function continuous at zero, there is a unique probability measure with that characteristic function, and the sequence converges weakly to it. Continuity is required only at zero; normalization of the limit follows from the probability measures in the sequence.

TauCeti.exists_probabilityMeasure_of_tendsto_charFun.{u_1} {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
  {μ : ℕ → MeasureTheory.ProbabilityMeasure E} {f : E → ℂ} (hf : ContinuousAt f 0)
  (h :
    ∀ (t : E),
      Filter.Tendsto (fun n => MeasureTheory.charFun (↑(μ n)) t) Filter.atTop (nhds (f t))) :
  ∃! μ₀, MeasureTheory.charFun ↑μ₀ = f ∧ Filter.Tendsto μ Filter.atTop (nhds μ₀)
Lean

Formalized in Tau Ceti as TauCeti.exists_probabilityMeasure_of_tendsto_charFun.

Sources
LeanTauCeti.exists_probabilityMeasure_of_tendsto_charFun
Used by 2
Used byBochner's theorem · Existence half of Bochner's theorem

TheoremProkhorov's theorem for finite measures#

A tight set of finite measures with uniformly bounded total mass has compact closure in the topology of weak convergence.

This is the finite-measure counterpart of Mathlib's isCompact_closure_of_isTightMeasureSet for probability measures.

TauCeti.isCompact_closure_of_isTightMeasureSet_of_mass_le.{u_1} {α : Type u_1} [MeasurableSpace α]
  [TopologicalSpace α] [T2Space α] [BorelSpace α] {S : Set (MeasureTheory.FiniteMeasure α)}
  {C : NNReal} (hTight : MeasureTheory.IsTightMeasureSet {x | ∃ μ ∈ S, ↑μ = x})
  (hmass : ∀ μ ∈ S, μ.mass ≤ C) : IsCompact (closure S)
Lean

Formalized in Tau Ceti as TauCeti.isCompact_closure_of_isTightMeasureSet_of_mass_le.

Other forms

Prokhorov's theorem along an ultrafilter, for measures carried by a compact set. Formalized in Tau Ceti as TauCeti.exists_tendsto_finiteMeasure_of_eventually_measure_compl_eq_zero.

TauCeti.exists_tendsto_finiteMeasure_of_eventually_measure_compl_eq_zero.{u_1, u_2} {α : Type u_1}
  [MeasurableSpace α] [TopologicalSpace α] [T2Space α] [BorelSpace α] {ι : Type u_2}
  {U : Ultrafilter ι} {μs : ι → MeasureTheory.FiniteMeasure α} {K : Set α} (hK : IsCompact K)
  {C : ℝ} (h : ∀ᶠ (i : ι) in ↑U, ↑(μs i) Kᶜ = 0 ∧ (↑(μs i)).real Set.univ ≤ C) :
  ∃ μ, ↑μ Kᶜ = 0 ∧ Filter.Tendsto μs (↑U) (nhds μ)
Sources
LeanTauCeti.isCompact_closure_of_isTightMeasureSet_of_mass_le · TauCeti.exists_tendsto_finiteMeasure_of_eventually_measure_compl_eq_zero
Used by 4
Used byHerglotz's theorem · Existence half of the Hausdorff--Bernstein--Widder theorem · Bernstein's theorem, existence half · The Herglotz representation theorem

TheoremSierpiński's theorem#

An atomless measure on a standard Borel space takes every value between 0 and μ s on measurable subsets of a measurable set s of finite measure.

MeasureTheory.Measure.exists_subset_measure_eq_of_nullSingleton.{u_1} {X : Type u_1}
  [MeasurableSpace X] [StandardBorelSpace X] (μ : MeasureTheory.Measure X)
  [MeasureTheory.NullSingletonClass μ] {s : Set X} (hs : MeasurableSet s) (hμs : μ s ≠ ⊤)
  {a : ENNReal} (ha : a ≤ μ s) : ∃ t ⊆ s, MeasurableSet t ∧ μ t = a
Lean

Formalized in Tau Ceti as MeasureTheory.Measure.exists_subset_measure_eq_of_nullSingleton.

Sources
LeanMeasureTheory.Measure.exists_subset_measure_eq_of_nullSingleton
Used by 1
Used byPratelli's theorem

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.