Measure theory

• Measurable spaces
• Sigma-algebras

InstanceProduct of sigma-algebras#

Mathlib states this as MeasurableSpace.pi.

MeasurableSpace.pi.{u_4, u_6} {δ : Type u_4} {X : δ → Type u_6}
  [m : (a : δ) → MeasurableSpace (X a)] : MeasurableSpace ((a : δ) → X a)

Sources

• Mathlib documentation: MeasurableSpace.pi
• Source of MeasurableSpace.pi in Mathlib/MeasureTheory/MeasurableSpace/Constructions.lean
• Mathlib undergraduate list: Measures and integral calculus › Measure theory
• Mathlib undergraduate list: Measures and integral calculus › Measure theory

MathlibMeasurableSpace.pi

Uses 1 · Used by 4

Statement usesEvents

Used byThe Birthday Problem · Product of finitely many measures · Gaussian processes · Ionescu-Tulcea theorem

• Borel sigma-algebras
• Positive measure

DefinitionCounting measure#

Counting measure on any measurable space.

MeasureTheory.Measure.count.{u_1} {α : Type u_1} [MeasurableSpace α] : MeasureTheory.Measure α

Sources

• Mathlib documentation: MeasureTheory.Measure.count
• Source of MeasureTheory.Measure.count in Mathlib/MeasureTheory/Measure/Count.lean
• Mathlib undergraduate list: Measures and integral calculus › Measure theory

MathlibMeasureTheory.Measure.count

Uses 2 · Used by 2

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

Used byThe Ballot Problem · The Birthday Problem

ClassLebesgue measure (Measure theory)#

A measure space is a measurable space equipped with a measure, referred to as volume.

MeasureTheory.MeasureSpace.{u_5} (α : Type u_5) : Type u_5

Sources

• Mathlib documentation: MeasureTheory.MeasureSpace
• Source of MeasureTheory.MeasureSpace in Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean
• Mathlib undergraduate list: Measures and integral calculus › Measure theory

MathlibMeasureTheory.MeasureSpace

Uses 1 · Used by 12

Statement usesPositive measure

Used byThe Birthday Problem · Fourier transform as an integral · Inversion formula · Riemann-Lebesgue lemma (Analysis) · Lebesgue measure (Measures and integral calculus) · Riemannian manifold · Strong law of large numbers · Fourier theorem · Dirichlet's approximation theorem · Fourier transforms on \(\mathcal{S}(\R^d)\) · Fourier transform on \(\mathrm{L}^2(\R^d)\) · Plancherel’s theorem

• Product measure
• Measurable functions

TheoremApproximation by step functions#

Mathlib states this as MeasureTheory.SimpleFunc.tendsto_approxOn.

MeasureTheory.SimpleFunc.tendsto_approxOn.{u_1, u_2} {α : Type u_1} {β : Type u_2}
  [MeasurableSpace α] [PseudoEMetricSpace α] [OpensMeasurableSpace α] [MeasurableSpace β]
  {f : β → α} (hf : Measurable f) {s : Set α} {y₀ : α} (h₀ : y₀ ∈ s)
  [TopologicalSpace.SeparableSpace ↑s] {x : β} (hx : f x ∈ closure s) :
  Filter.Tendsto (fun n => (MeasureTheory.SimpleFunc.approxOn f hf s y₀ h₀ n) x) Filter.atTop
    (nhds (f x))

Sources

• Mathlib documentation: MeasureTheory.SimpleFunc.tendsto_approxOn
• Source of MeasureTheory.SimpleFunc.tendsto_approxOn in Mathlib/MeasureTheory/Function/SimpleFuncDense.lean
• Mathlib undergraduate list: Measures and integral calculus › Measure theory

MathlibMeasureTheory.SimpleFunc.tendsto_approxOn

Uses 7 · Used by 4

Statement usesBorel sigma-algebra · Closure · Measurable function · Order topology · Real number

Proof usesContinuous function · Ordered ring

Used byDivergence theorem · Fubini's theorem · Strong law of large numbers · Borel-Cantelli lemma (difficult direction)

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.