28 Measure and integration

TheoremBounded convergence theorem #

Mathlib records this with 2 declarations.

MeasureTheory.FiniteMeasure.tendsto_lintegral_nn_of_le_const: A bounded convergence theorem for a finite measure: If a sequence of bounded continuous non-negative functions are uniformly bounded by a constant and tend pointwise to a limit, then their integrals (MeasureTheory.lintegral) against the finite measure tend to the integral of the limit.

A related result with more general assumptions is MeasureTheory.tendsto_lintegral_nn_filter_of_le_const.

MeasureTheory.FiniteMeasure.tendsto_lintegral_nn_of_le_const.{u_1} {Ω : Type u_1}
  [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω]
  (μ : MeasureTheory.FiniteMeasure Ω) {fs : ℕ → BoundedContinuousFunction Ω NNReal} {c : NNReal}
  (fs_le_const : ∀ (n : ℕ) (ω : Ω), (fs n) ω ≤ c) {f : Ω → NNReal}
  (fs_lim : ∀ (ω : Ω), Filter.Tendsto (fun n => (fs n) ω) Filter.atTop (nhds (f ω))) :
  Filter.Tendsto (fun n => ∫⁻ (ω : Ω), ↑((fs n) ω) ∂↑μ) Filter.atTop (nhds (∫⁻ (ω : Ω), ↑(f ω) ∂↑μ))

MeasureTheory.tendsto_lintegral_nn_filter_of_le_const: A bounded convergence theorem for a finite measure: If bounded continuous non-negative functions are uniformly bounded by a constant and tend to a limit, then their integrals against the finite measure tend to the integral of the limit. This formulation assumes: * the functions tend to a limit along a countably generated filter; * the limit is in the almost everywhere sense; * boundedness holds almost everywhere; * integration is MeasureTheory.lintegral, i.e., the functions and their integrals are ℝ≥0∞-valued.

MeasureTheory.tendsto_lintegral_nn_filter_of_le_const.{u_1, u_2} {Ω : Type u_1} [TopologicalSpace Ω]
  [MeasurableSpace Ω] [OpensMeasurableSpace Ω] {ι : Type u_2} {L : Filter ι}
  [L.IsCountablyGenerated] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ]
  {fs : ι → BoundedContinuousFunction Ω NNReal} {c : NNReal}
  (fs_le_const : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂μ, (fs i) ω ≤ c) {f : Ω → NNReal}
  (fs_lim : ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun i => (fs i) ω) L (nhds (f ω))) :
  Filter.Tendsto (fun i => ∫⁻ (ω : Ω), ↑((fs i) ω) ∂μ) L (nhds (∫⁻ (ω : Ω), ↑(f ω) ∂μ))

Sources

MathlibMeasureTheory.FiniteMeasure.tendsto_lintegral_nn_of_le_const · MeasureTheory.tendsto_lintegral_nn_filter_of_le_const

Uses 6

Statement usesAlmost sure convergence · Bornology · Continuous function · Integral of positive measurable functions · Order

Proof usesFatou's lemma

DefinitionCarathéodory's extension theorem #

Mathlib records this with 2 declarations.

MeasureTheory.AddContent.measure: Construct a measure from a sigma-subadditive content on a semiring, assuming the semiring generates a given measurable structure. The measure is defined on this measurable structure.

MeasureTheory.AddContent.measure.{u_1} {α : Type u_1} {C : Set (Set α)} [mα : MeasurableSpace α]
  (m : MeasureTheory.AddContent ENNReal C) (hC : MeasureTheory.IsSetSemiring C)
  (hC_gen : mα ≤ MeasurableSpace.generateFrom C) (m_sigma_subadd : m.IsSigmaSubadditive) :
  MeasureTheory.Measure α

MeasureTheory.AddContent.measure_eq: The measure defined through a sigma-subadditive content on a semiring coincides with the content on the semiring.

MeasureTheory.AddContent.measure_eq.{u_1} {α : Type u_1} {C : Set (Set α)} {s : Set α}
  [mα : MeasurableSpace α] (m : MeasureTheory.AddContent ENNReal C)
  (hC : MeasureTheory.IsSetSemiring C) (hC_gen : mα = MeasurableSpace.generateFrom C)
  (m_sigma_subadd : m.IsSigmaSubadditive) (hs : s ∈ C) : (m.measure hC ⋯ m_sigma_subadd) s = m s

Sources

MathlibMeasureTheory.AddContent.measure · MeasureTheory.AddContent.measure_eq

Uses 5 · Used by 2

Statement usesCarathéodory's theorem (measure theory) · Positive measure

Proof usesContinuous function · Hausdorff space · Order topology

Used byBinomial law · Ionescu-Tulcea theorem

DefinitionCarathéodory's theorem (measure theory)#

Given an outer measure μ, the Carathéodory-measurable space is defined such that s is measurable if ∀ t, μ t = μ (t ∩ s) + μ (t \ s).

MeasureTheory.OuterMeasure.caratheodory.{u} {α : Type u} (m : MeasureTheory.OuterMeasure α) :
  MeasurableSpace α

Hard to say what exactly is meant.

Sources

MathlibMeasureTheory.OuterMeasure.caratheodory

Uses 3 · Used by 63

Statement usesInfinite sum · Real number · Sigma-algebra

Used byFundamental Theorem of Integral Calculus · Minkowski’s Fundamental Theorem · Fourier Series · Cauchy integral formula · First Main Theorem of Value Distribution Theory · Riemann-Lebesgue lemma (Analysis) · Fundamental theorem of calculus, part 1 · Fundamental theorem of calculus, part 2 · Hausdorff measure · Uniform integrability · Approximation by convolution · Change of variables formula · Divergence theorem · Fubini's theorem · Product of finitely many measures · Regularization by convolution · Markov inequality · Strong law of large numbers · Conditional expectation · Conditional probability · Independent events · Independent sigma-algebras · Bernoulli law · Exponential law · Gaussian law · Geometric law · Independence of random variables · Mean of product of independent random variables · Poisson law · Probability density function · Haar measure on a locally compact Hausdorff group · Besicovitch covering theorem · Lebesgue differentiation theorem · Rademacher's theorem · Carathéodory's extension theorem · Prokhorov's theorem · Radon–Nikodym theorem · Steinhaus theorem · Vitali convergence theorem · Mellin inversion theorem · Morera's theorem · Poincaré recurrence theorem · Fourier theorem · Lebesgue's decomposition theorem · Lebesgue's density theorem · Dirichlet's approximation theorem · Continuous mapping theorem · Slutsky's theorem · Riemann-Lebesgue lemma (Measures and integral calculus) · Change of variables to polar co-ordinates · Continuity of integrals with respect to parameters · Differentiability of integrals with respect to parameters · Counting measure · Taylor's theorem with integral form for remainder (Differential calculus) · Cauchy-Lipschitz Theorem · Cauchy formulas · Holomorphic stability under uniform convergence · Antiderivative of a continuous function · Change of variable · Integration by parts · Comparison of a series and an integral · Taylor's theorem with integral form for remainder (Taylor-like theorems) · Example, the Hilbert basis of trigonometric polynomials

Dominated convergence theorem

TheoremEgorov's theorem #

Egorov's theorem: If f : ι → α → β is a sequence of strongly measurable functions that converges to g : α → β almost everywhere on a measurable set s of finite measure, then for all ε > 0, there exists a subset t ⊆ s such that μ t ≤ ε and f converges to g uniformly on s \ t. We require the index type ι to be countable, and usually ι = ℕ.

In other words, a sequence of almost everywhere convergent functions converges uniformly except on an arbitrarily small set.

MeasureTheory.tendstoUniformlyOn_of_ae_tendsto.{u_1, u_2, u_3} {α : Type u_1} {β : Type u_2}
  {ι : Type u_3} {m : MeasurableSpace α} [PseudoEMetricSpace β] {μ : MeasureTheory.Measure α}
  [SemilatticeSup ι] [Nonempty ι] [Countable ι] {f : ι → α → β} {g : α → β} {s : Set α}
  {ε : ENNReal} (hf : ∀ (n : ι), MeasureTheory.StronglyMeasurable (f n))
  (hg : MeasureTheory.StronglyMeasurable g) (hsm : MeasurableSet s) (hs : μ s ≠ ⊤)
  (hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (g x)))
  (hε : 0 < ε) : ∃ t ⊆ s, MeasurableSet t ∧ μ t ≤ ε ∧ TendstoUniformlyOn f g Filter.atTop (s \ t)

Sources

MathlibMeasureTheory.tendstoUniformlyOn_of_ae_tendsto

Uses 7

Statement usesAlmost sure convergence · Positive measure

Proof usesBorel sigma-algebra · Measurable function · Pointwise convergence · Sum of a Geometric Series · Uniform convergence norm (sup-norm)

TheoremFernique's theorem #

Fernique's theorem: for a Gaussian measure, there exists C > 0 such that the function x ↦ exp (C * ‖x‖ ^ 2) is integrable.

ProbabilityTheory.IsGaussian.exists_integrable_exp_sq.{u_1} {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] [CompleteSpace E]
  (μ : MeasureTheory.Measure E) [ProbabilityTheory.IsGaussian μ] :
  ∃ C, 0 < C ∧ MeasureTheory.Integrable (fun x => Real.exp (C * ‖x‖ ^ 2)) μ

Sources

MathlibProbabilityTheory.IsGaussian.exists_integrable_exp_sq

Uses 10

Statement usesGaussian measures

Proof usesCharacteristic zero · Field \(\C\) of complex numbers · Fubini's theorem · Probability measure · Product of vector spaces · The Binomial Theorem · The Triangle Inequality · Topological ring · Trigonometric functions

Fubini's theorem

TheoremHahn decomposition theorem #

The Hahn decomposition theorem: Given a signed measure s, there exist complement measurable sets i and j such that i is positive, j is negative.

MeasureTheory.SignedMeasure.exists_isCompl_positive_negative.{u_1} {α : Type u_1}
  [MeasurableSpace α] (s : MeasureTheory.SignedMeasure α) :
  ∃ i j,
    MeasurableSet i ∧
      MeasureTheory.VectorMeasure.restrict 0 i ≤ MeasureTheory.VectorMeasure.restrict s i ∧
        MeasurableSet j ∧
          MeasureTheory.VectorMeasure.restrict s j ≤ MeasureTheory.VectorMeasure.restrict 0 j ∧
            IsCompl i j

Sources

MathlibMeasureTheory.SignedMeasure.exists_isCompl_positive_negative

Uses 10

Statement usesBornology · Events · Infinite sum · Order

Proof usesCharacteristic zero · Completeness of R · Hausdorff space · Metric structure · Order topology · Uniformly continuous function

TheoremProkhorov's theorem #

Mathlib records this with 4 declarations.

isCompact_setOfPred_finiteMeasure_mass_le_compl_isCompact_le: Prokhorov theorem: Given a sequence of compact sets Kₙ and a sequence uₙ tending to zero, the finite measures of mass at most C giving mass at most uₙ to the complement of Kₙ form a compact set.

isCompact_setOfPred_finiteMeasure_mass_le_compl_isCompact_le.{u_1} {E : Type u_1}
  [MeasurableSpace E] [TopologicalSpace E] [T2Space E] [BorelSpace E] {u : ℕ → NNReal}
  {K : ℕ → Set E} (C : NNReal) (hu : Filter.Tendsto u Filter.atTop (nhds 0))
  (hK : ∀ (n : ℕ), IsCompact (K n)) (h : NormalSpace E ∨ Monotone K) :
  IsCompact {μ | μ.mass ≤ C ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n}

isCompact_setOfPred_finiteMeasure_mass_eq_compl_isCompact_le: Prokhorov theorem: Given a sequence of compact sets Kₙ and a sequence uₙ tending to zero, the finite measures of mass C giving mass at most uₙ to the complement of Kₙ form a compact set.

isCompact_setOfPred_finiteMeasure_mass_eq_compl_isCompact_le.{u_1} {E : Type u_1}
  [MeasurableSpace E] [TopologicalSpace E] [T2Space E] [BorelSpace E] {u : ℕ → NNReal}
  {K : ℕ → Set E} (C : NNReal) (hu : Filter.Tendsto u Filter.atTop (nhds 0))
  (hK : ∀ (n : ℕ), IsCompact (K n)) (h : NormalSpace E ∨ Monotone K) :
  IsCompact {μ | μ.mass = C ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n}

isCompact_setOfPred_probabilityMeasure_mass_eq_compl_isCompact_le: Prokhorov theorem: Given a sequence of compact sets Kₙ and a sequence uₙ tending to zero, the probability measures giving mass at most uₙ to the complement of Kₙ form a compact set.

isCompact_setOfPred_probabilityMeasure_mass_eq_compl_isCompact_le.{u_1} {E : Type u_1}
  [MeasurableSpace E] [TopologicalSpace E] [T2Space E] [BorelSpace E] {u : ℕ → NNReal}
  {K : ℕ → Set E} (hu : Filter.Tendsto u Filter.atTop (nhds 0)) (hK : ∀ (n : ℕ), IsCompact (K n))
  (h : NormalSpace E ∨ Monotone K) : IsCompact {μ | ∀ (n : ℕ), μ (K n)ᶜ ≤ u n}

isCompact_closure_of_isTightMeasureSet: Prokhorov theorem: the closure of a tight set of probability measures is compact. We only require the space to be T2.

isCompact_closure_of_isTightMeasureSet.{u_1} {E : Type u_1} [MeasurableSpace E] [TopologicalSpace E]
  [T2Space E] [BorelSpace E] {S : Set (MeasureTheory.ProbabilityMeasure E)}
  (hS : MeasureTheory.IsTightMeasureSet {x | ∃ μ ∈ S, ↑μ = x}) : IsCompact (closure S)

Sources

MathlibisCompact_setOfPred_finiteMeasure_mass_le_compl_isCompact_le · isCompact_setOfPred_finiteMeasure_mass_eq_compl_isCompact_le · isCompact_setOfPred_probabilityMeasure_mass_eq_compl_isCompact_le · isCompact_closure_of_isTightMeasureSet

Uses 12 · Used by 1

Statement usesBorel sigma-algebra · Closure · Compactness in terms of filters · Hausdorff space · Probability measure

Proof usesBochner integral · Carathéodory's theorem (measure theory) · Completeness of R · Heine-Borel theorem (proper metric space version) · Inner product space, over \(R\) or \(C\) · Measurable function · Urysohn's lemma

Used byLévy continuity theorem

TheoremRadon–Nikodym theorem #

The Radon-Nikodym theorem: Given two measures μ and ν, if HaveLebesgueDecomposition μ ν, then μ is absolutely continuous to ν if and only if ν.withDensity (rnDeriv μ ν) = μ.

MeasureTheory.Measure.absolutelyContinuous_iff_withDensity_rnDeriv_eq.{u_1} {α : Type u_1}
  {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [μ.HaveLebesgueDecomposition ν] :
  μ.AbsolutelyContinuous ν ↔ ν.withDensity (μ.rnDeriv ν) = μ

Sources

MathlibMeasureTheory.Measure.absolutelyContinuous_iff_withDensity_rnDeriv_eq

Uses 5

Statement usesAssociative algebra over a commutative ring · Carathéodory's theorem (measure theory) · Integral of positive measurable functions · Linear map · Measurable function

DefinitionSchroeder–Bernstein theorem for measurable spaces #

The measurable Schröder-Bernstein Theorem: given measurable embeddings α → β and β → α, we can find a measurable equivalence α ≃ᵐ β.

MeasurableEmbedding.schroederBernstein.{u_1, u_2} {α : Type u_1} {β : Type u_2} [MeasurableSpace α]
  [MeasurableSpace β] {f : α → β} {g : β → α} (hf : MeasurableEmbedding f)
  (hg : MeasurableEmbedding g) : α ≃ᵐ β

Sources

MathlibMeasurableEmbedding.schroederBernstein

Uses 1

Statement usesMeasurable function

TheoremSteinhaus theorem #

Steinhaus Theorem.

In any locally compact group G with an inner regular Haar measure μ, for any measurable set E of positive measure, the set E / E is a neighbourhood of 1.

MeasureTheory.Measure.div_mem_nhds_one_of_haar_pos.{u_1} {G : Type u_1} [Group G]
  [TopologicalSpace G] [IsTopologicalGroup G] [MeasurableSpace G] [BorelSpace G]
  (μ : MeasureTheory.Measure G) [μ.IsHaarMeasure] [LocallyCompactSpace G] [μ.InnerRegular]
  (E : Set G) (hE : MeasurableSet E) (hEpos : 0 < μ E) : E / E ∈ nhds 1

Sources

MathlibMeasureTheory.Measure.div_mem_nhds_one_of_haar_pos

Uses 10

Statement usesAlmost sure convergence · Associative algebra over a commutative ring · Borel sigma-algebra · Carathéodory's theorem (measure theory) · Compactness in terms of filters · Linear map · Measurable function · Positive measure · Topological group

Proof usesClosure

TheoremVitali convergence theorem #

Vitali's convergence theorem (non-finite measure version).

A sequence of functions f converges to g in Lp if and only if it is uniformly integrable, uniformly tight and converges to g in measure.

MeasureTheory.tendstoInMeasure_iff_tendsto_Lp.{u_1, u_2} {α : Type u_1} {β : Type u_2}
  {m : MeasurableSpace α} [NormedAddCommGroup β] {μ : MeasureTheory.Measure α} {p : ENNReal}
  {f : ℕ → α → β} {g : α → β} (hp : 1 ≤ p) (hp' : p ≠ ⊤)
  (hf : ∀ (n : ℕ), MeasureTheory.MemLp (f n) p μ) (hg : MeasureTheory.MemLp g p μ) :
  MeasureTheory.TendstoInMeasure μ f Filter.atTop g ∧
      MeasureTheory.UnifIntegrable f p μ ∧ MeasureTheory.UnifTight f p μ ↔
    Filter.Tendsto (fun n => MeasureTheory.eLpNorm (f n - g) p μ) Filter.atTop (nhds 0)

Sources

MathlibMeasureTheory.tendstoInMeasure_iff_tendsto_Lp

Uses 13

Statement usesAlmost sure convergence · Associative algebra over a commutative ring · Carathéodory's theorem (measure theory) · Continuous function · Convergence in probability · Integral of positive measurable functions · Linear map · Metric space

Proof usesBorel-Cantelli lemma (easy direction) · Characteristic zero · Closure · Cluster point · Ordered ring

TheoremVitali covering theorem #

The measurable Vitali covering theorem.

Assume one is given a family t of closed sets with nonempty interior, such that each a ∈ t is included in a ball B (x, r) and covers a definite proportion of the ball B (x, 3 r) for a given measure μ (think of the situation where μ is a doubling measure and t is a family of balls). Consider a \(possibly non-measurable\) set s at which the family is fine, i.e., every point of s belongs to arbitrarily small elements of t. Then one can extract from t a disjoint subfamily that covers almost all s.

For more flexibility, we give a statement with a parameterized family of sets.

Vitali.exists_disjoint_covering_ae.{u_1, u_2} {α : Type u_1} {ι : Type u_2} [PseudoMetricSpace α]
  [MeasurableSpace α] [OpensMeasurableSpace α] [SecondCountableTopology α]
  (μ : MeasureTheory.Measure α) [MeasureTheory.IsLocallyFiniteMeasure μ] (s : Set α) (t : Set ι)
  (C : NNReal) (r : ι → ℝ) (c : ι → α) (B : ι → Set α)
  (hB : ∀ a ∈ t, B a ⊆ Metric.closedBall (c a) (r a))
  (μB : ∀ a ∈ t, μ (Metric.closedBall (c a) (3 * r a)) ≤ ↑C * μ (B a))
  (ht : ∀ a ∈ t, (interior (B a)).Nonempty) (h't : ∀ a ∈ t, IsClosed (B a))
  (hf : ∀ x ∈ s, ∀ ε > 0, ∃ a ∈ t, r a ≤ ε ∧ c a = x) :
  ∃ u ⊆ t, u.Countable ∧ u.PairwiseDisjoint B ∧ μ (s \ ⋃ a ∈ u, B a) = 0

Sources

MathlibVitali.exists_disjoint_covering_ae

Uses 8

Statement usesBornology · Order · Positive measure

Proof usesCharacteristic zero · Closure · Order topology · Topological ring · Topology of a metric space

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

28 Measure and integration

TheoremBounded convergence theorem#

Sources

DefinitionCarathéodory's extension theorem#

Sources

DefinitionCarathéodory's theorem (measure theory)#

Sources

TheoremEgorov's theorem#

Sources

TheoremFernique's theorem#

Sources

TheoremHahn decomposition theorem#

Sources

TheoremProkhorov's theorem#

Sources

TheoremRadon–Nikodym theorem#

Sources

DefinitionSchroeder–Bernstein theorem for measurable spaces#

Sources

TheoremSteinhaus theorem#

Sources

TheoremVitali convergence theorem#

Sources

TheoremVitali covering theorem#

Sources

TheoremBounded convergence theorem #

DefinitionCarathéodory's extension theorem #

TheoremEgorov's theorem #

TheoremFernique's theorem #

TheoremHahn decomposition theorem #

TheoremProkhorov's theorem #

TheoremRadon–Nikodym theorem #

DefinitionSchroeder–Bernstein theorem for measurable spaces #

TheoremSteinhaus theorem #

TheoremVitali convergence theorem #

TheoremVitali covering theorem #