Sigma-algebra to Fundamental theorem of…

ClassSigma-algebra#

A measurable space is a space equipped with a σ-algebra.

MeasurableSpace.{u_6} (α : Type u_6) : Type u_6
Sources
MathlibMeasurableSpace
Uses 1 · Used by 4
Statement usesNatural number
Used byBorel sigma-algebra · The category of measurable spaces · Carathéodory's theorem (measure theory) · Events

DefinitionMeasurable function#

A function f between measurable spaces is measurable if the preimage of every measurable set is measurable.

Measurable.{u_1, u_2} {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β]
  (f : α → β) : Prop
Sources
MathlibMeasurable
Uses 1 · Used by 41
Statement usesEvents
Used byFundamental Theorem of Integral Calculus · Minkowski’s Fundamental Theorem · Buffon Needle Problem · Jensen's inequality (integral version) · Riemann-Lebesgue lemma (Analysis) · Fatou's lemma · Fundamental theorem of calculus, part 2 · Monotone convergence theorem (Measures and integral calculus) · Approximation by convolution · Change of variables formula · Fubini's theorem · Regularization by convolution · Markov inequality · Strong law of large numbers · Independent events · Independent sigma-algebras · Binomial law · Gaussian measures · Independence of random variables · Mean of product of independent random variables · Probability density function · Lebesgue differentiation theorem · Monotone convergence theorem (1000+ theorems) · Rademacher's theorem · Egorov's theorem · Prokhorov's theorem · Radon–Nikodym theorem · Schroeder–Bernstein theorem for measurable spaces · Steinhaus theorem · Poincaré recurrence theorem · Fourier theorem · Lebesgue's decomposition theorem · Dirichlet's approximation theorem · Continuous mapping theorem · Ionescu-Tulcea theorem · Slutsky's theorem · Riemann-Lebesgue lemma (Measures and integral calculus) · Hölder's inequality · Approximation by step functions · Comparison of a series and an integral · Completeness of \(L^2\)

StructureThe category of measurable spaces#

The category of measurable spaces and measurable functions.

MeasCat.{u} : Type (u + 1)
Sources
MathlibMeasCat
Uses 1
Statement usesSigma-algebra

ClassBorel sigma-algebra#

A space with MeasurableSpace and TopologicalSpace structures such that the σ-algebra of measurable sets is exactly the σ-algebra generated by open sets.

BorelSpace.{u_6} (α : Type u_6) [TopologicalSpace α] [MeasurableSpace α] : Prop
Sources
MathlibBorelSpace
Uses 2 · Used by 41
Statement usesSigma-algebra · Topological space
Used byMinkowski’s Fundamental Theorem · Fourier Series · Jensen's inequality (integral version) · Fourier transform as an integral · Inversion formula · Riemann-Lebesgue lemma (Analysis) · Fatou's lemma · Hausdorff measure · Lebesgue measure (Measures and integral calculus) · Monotone convergence theorem (Measures and integral calculus) · Stieltjes measure · Approximation by convolution · Change of variables formula · Regularization by convolution · Markov inequality · Strong law of large numbers · Kolmogorov's \(0\)-\(1\) law · Haar measure on a locally compact Hausdorff group · Lebesgue differentiation theorem · Monotone convergence theorem (1000+ theorems) · Rademacher's theorem · Egorov's theorem · Prokhorov's theorem · Steinhaus theorem · Fourier theorem · Lebesgue's density theorem · Dirichlet's approximation theorem · Continuous mapping theorem · Lévy continuity theorem · Slutsky's theorem · Poisson’s formula · Convolution of two functions of \(\mathcal{S}(\R^d)\) · Fourier transforms on \(\mathcal{S}(\R^d)\) · \(L^p\) functions · Fourier transform on \(\mathrm{L}^2(\R^d)\) · Plancherel’s theorem · Riemann-Lebesgue lemma (Measures and integral calculus) · Continuity of integrals with respect to parameters · Approximation by step functions · Completeness of \(L^2\) · Example, the Hilbert basis of trigonometric polynomials

StructurePositive measure#

A measure is defined to be an outer measure that is countably additive on measurable sets, with the additional assumption that the outer measure is the canonical extension of the restricted measure.

The measure of a set s, denoted μ s, is an extended nonnegative real. The real-valued version is written μ.real s.

MeasureTheory.Measure.{u_5} (α : Type u_5) [MeasurableSpace α] : Type u_5
Sources
MathlibMeasureTheory.Measure
Uses 3 · Used by 23
Statement usesEvents · Infinite sum · Real number
Used byMinkowski’s Fundamental Theorem · Giry monad · Hausdorff measure · Integral of positive measurable functions · Stieltjes measure · Product of finitely many measures · Convergence in probability · Conditional probability · Probability measure · Bernoulli law · Geometric law · Poisson law · Haar measure on a locally compact Hausdorff group · Besicovitch covering theorem · Rademacher's theorem · Carathéodory's extension theorem · Egorov's theorem · Steinhaus theorem · Vitali covering theorem · Poincaré recurrence theorem · Lebesgue's density theorem · Counting measure · Lebesgue measure (Measure theory)

DefinitionStieltjes measure#

The measure associated to a Stieltjes function, giving mass f b - f a to the interval (a, b]. If there is a bot element, it gives zero mass to it.

StieltjesFunction.measure.{u_1} {R : Type u_1} [LinearOrder R] [TopologicalSpace R]
  (f : StieltjesFunction R) [OrderTopology R] [CompactIccSpace R] [MeasurableSpace R] [BorelSpace R]
  [SecondCountableTopology R] [DenselyOrdered R] : MeasureTheory.Measure R
Sources
MathlibStieltjesFunction.measure
Uses 6
Statement usesBorel sigma-algebra · Bornology · Compactness in terms of filters · Order · Order topology · Positive measure

InstanceLebesgue measure (Measures and integral calculus)#

Mathlib states this as Real.measureSpace.

Real.measureSpace : MeasureTheory.MeasureSpace ℝ
Sources
MathlibReal.measureSpace
Uses 4 · Used by 26
Statement usesBorel sigma-algebra · Finite-dimensionality · Inner product space, over \(R\) or \(C\) · Lebesgue measure (Measure theory)
Used byFundamental Theorem of Integral Calculus · The Area of a Circle · Buffon Needle Problem · Cauchy integral formula · First Main Theorem of Value Distribution Theory · Fundamental theorem of calculus, part 1 · Fundamental theorem of calculus, part 2 · Divergence theorem · Dirichlet class number formula · Exponential law · Gaussian law · Rademacher's theorem · Mellin inversion theorem · Morera's theorem · Poisson’s formula · Change of variables to polar co-ordinates · Differentiability of integrals with respect to parameters · 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)

DefinitionHausdorff measure#

Hausdorff measure on an (e)metric space.

MeasureTheory.Measure.hausdorffMeasure.{u_2} {X : Type u_2} [EMetricSpace X] [MeasurableSpace X]
  [BorelSpace X] (d : ℝ) : MeasureTheory.Measure X
Sources
MathlibMeasureTheory.Measure.hausdorffMeasure
Uses 3 · Used by 1
Statement usesBorel sigma-algebra · Carathéodory's theorem (measure theory) · Positive measure
Used byHausdorff dimension

DefinitionHausdorff dimension#

Hausdorff dimension of a set in an (e)metric space.

dimH.{u_2} {X : Type u_2} [EMetricSpace X] (s : Set X) : ENNReal
Sources
MathlibdimH
Uses 1
Statement usesHausdorff measure

InstanceGiry monad#

Measurability structure on Measure: Measures are measurable w.r.t. all projections

MeasureTheory.Measure.instMeasurableSpace.{u_1} {α : Type u_1} {mα : MeasurableSpace α} :
  MeasurableSpace (MeasureTheory.Measure α)
Sources
MathlibMeasureTheory.Measure.instMeasurableSpace
Uses 1 · Used by 9
Statement usesPositive measure
Used byThe Area of a Circle · Fubini's theorem · Strong law of large numbers · Independent events · Independent sigma-algebras · Independence of random variables · Mean of product of independent random variables · Ionescu-Tulcea theorem · Change of variables to polar co-ordinates

DefinitionIntegral of positive measurable functions#

The lower Lebesgue integral of a function f with respect to a measure μ.

MeasureTheory.lintegral.{u_1} {α : Type u_1} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α)
  (f : α → ENNReal) : ENNReal
Sources
MathlibMeasureTheory.lintegral
Uses 1 · Used by 16
Statement usesPositive measure
Used byFatou's lemma · \(L^p\) space · Monotone convergence theorem (Measures and integral calculus) · Uniform integrability · Vector-valued integrable function (Bochner integral) · Riemannian manifold · Markov inequality · Gaussian law · Probability density function · Lebesgue differentiation theorem · Bounded convergence theorem · Radon–Nikodym theorem · Vitali convergence theorem · Lebesgue's decomposition theorem · Ionescu-Tulcea theorem · Hölder's inequality

TheoremMonotone convergence theorem (Measures and integral calculus)#

Monotone convergence theorem for nonincreasing sequences of functions.

MeasureTheory.lintegral_iInf_ae.{u_1} {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α} {f : ℕ → α → ENNReal} (h_meas : ∀ (n : ℕ), Measurable (f n))
  (h_mono : ∀ (n : ℕ), f n.succ ≤ᵐ[μ] f n) (h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤) :
  ∫⁻ (a : α), ⨅ n, f n a ∂μ = ⨅ n, ∫⁻ (a : α), f n a ∂μ
Sources
MathlibMeasureTheory.lintegral_iInf_ae
Uses 5
Statement usesAlmost sure convergence · Integral of positive measurable functions · Measurable function
Proof usesBorel sigma-algebra · Order topology

TheoremFatou's lemma#

Fatou's lemma, version with Measurable functions.

MeasureTheory.lintegral_liminf_le.{u_1, u_3} {α : Type u_1} {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {ι : Type u_3} {f : ι → α → ENNReal} {u : Filter ι}
  [u.IsCountablyGenerated] (h_meas : ∀ (i : ι), Measurable (f i)) :
  ∫⁻ (a : α), Filter.liminf (fun i => f i a) u ∂μ ≤ Filter.liminf (fun i => ∫⁻ (a : α), f i a ∂μ) u
Sources
MathlibMeasureTheory.lintegral_liminf_le
Uses 9 · Used by 2
Statement usesIntegral of positive measurable functions · Measurable function
Proof usesAlmost sure convergence · Borel sigma-algebra · Closure · Cluster point · Metric space · Order topology · Ordered ring
Used byBounded convergence theorem · Slutsky's theorem

DefinitionVector-valued integrable function (Bochner integral)#

Integrable f μ means that f is measurable and that the integral ∫⁻ a, ‖f a‖ ∂μ is finite. Integrable f means Integrable f volume.

MeasureTheory.Integrable.{u_5, u_7} {ε : Type u_5} [TopologicalSpace ε] [ContinuousENorm ε]
  {α : Type u_7} {x✝ : MeasurableSpace α} (f : α → ε)
  (μ : MeasureTheory.Measure α := by volume_tac) : Prop
Sources
MathlibMeasureTheory.Integrable
Uses 3 · Used by 6
Statement usesAlmost sure convergence · Continuous function · Integral of positive measurable functions
Used byInversion formula · Bochner integral · Conditional expectation · Fourier theorem · \(L^p\) functions · Fourier transform on \(\mathrm{L}^2(\R^d)\)

StructureUniform integrability#

In probability theory, a family of measurable functions is uniformly integrable if it is uniformly integrable in the measure theory sense and is uniformly bounded.

MeasureTheory.UniformIntegrable.{u_1, u_2, u_3} {α : Type u_1} {β : Type u_2} {ι : Type u_3}
  {m : MeasurableSpace α} [NormedAddCommGroup β] (f : ι → α → β) (p : ENNReal)
  (μ : MeasureTheory.Measure α) : Prop
Sources
MathlibMeasureTheory.UniformIntegrable
Uses 7
Statement usesAlmost sure convergence · Associative algebra over a commutative ring · Carathéodory's theorem (measure theory) · Continuous function · Integral of positive measurable functions · Linear map · Metric space

Definition\(L^p\) space#

Lp space

MeasureTheory.Lp.{u_6, u_7} {α : Type u_7} (E : Type u_6) {m : MeasurableSpace α}
  [NormedAddCommGroup E] (p : ENNReal) (μ : MeasureTheory.Measure α := by volume_tac) :
  AddSubgroup (α →ₘ[μ] E)
Sources
MathlibMeasureTheory.Lp
Uses 4 · Used by 5
Statement usesAlmost sure convergence · Continuous function · Integral of positive measurable functions · Metric space
Used byBochner integral · \(L^p\) functions · Fourier transform on \(\mathrm{L}^2(\R^d)\) · Completeness of \(L^2\) · Inner product space \(L^2\)

DefinitionBochner integral#

The Bochner integral

MeasureTheory.integral.{u_1, u_5} {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G]
  [NormedSpace ℝ G] {x✝ : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : α → G) : G
Sources
MathlibMeasureTheory.integral
Uses 6 · Used by 44
Statement uses\(L^p\) space · Completeness · Extension by continuity · Norm of a continuous linear map · Normed vector space over a normed field · Vector-valued integrable function (Bochner integral)
Used byFundamental Theorem of Integral Calculus · Fourier Series · Buffon Needle Problem · Cauchy integral formula · First Main Theorem of Value Distribution Theory · Jensen's inequality (integral version) · Fourier transform as an integral · Riemann-Lebesgue lemma (Analysis) · Dominated convergence theorem · Fundamental theorem of calculus, part 1 · Fundamental theorem of calculus, part 2 · Change of variables formula · Convolution · Divergence theorem · Fubini's theorem · Convergence in distribution · Strong law of large numbers · Characteristic function · Exponential law · Mean of product of independent random variables · Moment of a random variable · Variance of a real-valued random variable · Optional stopping theorem · Monotone convergence theorem (1000+ theorems) · Prokhorov's theorem · Mellin inversion theorem · Morera's theorem · Fourier theorem · Fourier transforms on \(\mathcal{S}(\R^d)\) · Plancherel’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 · Taylor's theorem with integral form for remainder (Differential calculus) · Cauchy-Lipschitz Theorem · Borel-Cantelli lemma (difficult direction) · 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)

TheoremDominated convergence theorem#

Lebesgue dominated convergence theorem provides sufficient conditions under which almost everywhere convergence of a sequence of functions implies the convergence of their integrals. We could weaken the condition bound_integrable to require HasFiniteIntegral bound μ instead (i.e. not requiring that bound is measurable), but in all applications proving integrability is easier.

MeasureTheory.tendsto_integral_of_dominated_convergence.{u_1, u_3} {α : Type u_1} {G : Type u_3}
  [NormedAddCommGroup G] [NormedSpace ℝ G] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {F : ℕ → α → G} {f : α → G} (bound : α → ℝ)
  (F_measurable : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (F n) μ)
  (bound_integrable : MeasureTheory.Integrable bound μ)
  (h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a)
  (h_lim : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun n => F n a) Filter.atTop (nhds (f a))) :
  Filter.Tendsto (fun n => ∫ (a : α), F n a ∂μ) Filter.atTop (nhds (∫ (a : α), f a ∂μ))
Sources
MathlibMeasureTheory.tendsto_integral_of_dominated_convergence
Uses 1 · Used by 3
Statement usesBochner integral
Used byRademacher's theorem · Lévy continuity theorem · Riemann-Lebesgue lemma (Measures and integral calculus)

TheoremFundamental theorem of calculus, part 1#

Fundamental theorem of calculus-1: if f : ℝ → E is integrable on a..b and f x has finite limits ca and cb almost surely as x tends to a and b, respectively, then (u, v) ↦ ∫ x in u..v, f x has derivative (u, v) ↦ v • cb - u • ca at (a, b).

intervalIntegral.integral_hasFDerivAt_of_tendsto_ae.{u_3} {E : Type u_3} [NormedAddCommGroup E]
  [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} {ca cb : E} {a b : ℝ}
  (hf : IntervalIntegrable f MeasureTheory.volume a b)
  (hmeas_a : StronglyMeasurableAtFilter f (nhds a) MeasureTheory.volume)
  (hmeas_b : StronglyMeasurableAtFilter f (nhds b) MeasureTheory.volume)
  (ha : Filter.Tendsto f (nhds a ⊓ MeasureTheory.ae MeasureTheory.volume) (nhds ca))
  (hb : Filter.Tendsto f (nhds b ⊓ MeasureTheory.ae MeasureTheory.volume) (nhds cb)) :
  HasFDerivAt (fun p => ∫ (x : ℝ) in p.1..p.2, f x)
    ((ContinuousLinearMap.snd ℝ ℝ ℝ).smulRight cb - (ContinuousLinearMap.fst ℝ ℝ ℝ).smulRight ca)
    (a, b)
Sources
MathlibintervalIntegral.integral_hasFDerivAt_of_tendsto_ae
Uses 8
Statement usesBochner integral · Carathéodory's theorem (measure theory) · Differentiable function between normed vector spaces · Lebesgue measure (Measures and integral calculus) · Product of vector spaces · Topological module
Proof usesCompleteness of R · Order topology

TheoremFundamental theorem of calculus, part 2#

Fundamental theorem of calculus-2: If f : ℝ → E is continuous on [a, b] (where a ≤ b) and has a right derivative at f' x for all x in (a, b), and f' is integrable on [a, b], then ∫ y in a..b, f' y equals f b - f a.

intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le.{u_3} {E : Type u_3} [NormedAddCommGroup E]
  [NormedSpace ℝ E] {a b : ℝ} [CompleteSpace E] {f f' : ℝ → E} (hab : a ≤ b)
  (hcont : ContinuousOn f (Set.Icc a b))
  (hderiv : ∀ x ∈ Set.Ioo a b, HasDerivWithinAt f (f' x) (Set.Ioi x) x)
  (f'int : IntervalIntegrable f' MeasureTheory.volume a b) : ∫ (y : ℝ) in a..b, f' y = f b - f a
Sources
MathlibintervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le
Uses 15 · Used by 6
Statement usesBochner integral · Carathéodory's theorem (measure theory) · Lebesgue measure (Measures and integral calculus) · Topological module
Proof usesAffine space · Compactness in terms of filters · Completeness of R · Differentiable function between normed vector spaces · Dual of a normed space · Extended real number · Local convexity · Measurable function · Metric structure · Order topology · Topological ring
Used byEuler’s Summation of 1 + (1/2)^2 + (1/3)^2 + …. · The Area of a Circle · Taylor's theorem with integral form for remainder (Differential calculus) · Log · Change of variable · Integration by parts

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.