Integration

TheoremContinuity of integrals with respect to parameters#

Continuity of interval integral with respect to a parameter. Given F : X → ℝ → E, assume each F x is ae-measurable on [a, b], and assume it is bounded by a function integrable on [a, b] independent of x. If (fun x ↦ F x t) is continuous for almost every t in [a, b] then the same holds for (fun x ↦ ∫ t in a..b, F x t ∂μ) s x₀.

intervalIntegral.continuous_of_dominated_interval.{u_2, u_3} {E : Type u_2} [NormedAddCommGroup E]
  [NormedSpace ℝ E] {μ : MeasureTheory.Measure ℝ} {X : Type u_3} [TopologicalSpace X]
  [FirstCountableTopology X] {F : X → ℝ → E} {bound : ℝ → ℝ} {a b : ℝ}
  (hF_meas : ∀ (x : X), MeasureTheory.AEStronglyMeasurable (F x) (μ.restrict (Set.uIoc a b)))
  (h_bound : ∀ (x : X), ∀ᵐ (t : ℝ) ∂μ, t ∈ Set.uIoc a b → ‖F x t‖ ≤ bound t)
  (bound_integrable : IntervalIntegrable bound μ a b)
  (h_cont : ∀ᵐ (t : ℝ) ∂μ, t ∈ Set.uIoc a b → Continuous fun x => F x t) :
  Continuous fun x => ∫ (t : ℝ) in a..b, F x t ∂μ
Sources
MathlibintervalIntegral.continuous_of_dominated_interval
Uses 6
Statement usesAssociative algebra over a commutative ring · Bochner integral · Carathéodory's theorem (measure theory)
Proof usesBorel sigma-algebra · Metric structure · Topological module

TheoremDifferentiability of integrals with respect to parameters#

The (local) interval version of the Lebesgue Differentiation Theorem: if f : ℝ → E is interval integrable on a..b, then for almost every x ∈ uIcc a b, for any c ∈ uIcc a b, the derivative of ∫ (t : ℝ) in c..x, f t at x is equal to f x.

IntervalIntegrable.ae_hasDerivAt_integral.{u_1} {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} {a b : ℝ}
  (hf : IntervalIntegrable f MeasureTheory.volume a b) :
  ∀ᵐ (x : ℝ),
    x ∈ Set.uIcc a b → ∀ c ∈ Set.uIcc a b, HasDerivAt (fun x => ∫ (t : ℝ) in c..x, f t) (f x) x
Sources
MathlibIntervalIntegrable.ae_hasDerivAt_integral
Uses 7 · Used by 1
Statement usesBochner integral · Carathéodory's theorem (measure theory) · Derivative at a point · Lebesgue measure (Measures and integral calculus)
Proof usesAffine space · Compactness in terms of filters · Lebesgue's decomposition theorem
Used byTaylor's theorem with integral form for remainder (Taylor-like theorems)

TheoremHölder's inequality#

Hölder's inequality for functions α → ℝ≥0. The integral of the product of two functions is bounded by the product of their ℒp and ℒq seminorms when p and q are conjugate exponents.

NNReal.lintegral_mul_le_Lp_mul_Lq.{u_1} {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α} {p q : ℝ} (hpq : p.HolderConjugate q) {f g : α → NNReal}
  (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
  ∫⁻ (a : α), ↑((f * g) a) ∂μ ≤
    (∫⁻ (a : α), ↑(f a) ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), ↑(g a) ^ q ∂μ) ^ (1 / q)
Sources
MathlibNNReal.lintegral_mul_le_Lp_mul_Lq
Uses 4
Statement usesAlmost sure convergence · Integral of positive measurable functions · Measurable function
Proof usesArithmetic Mean/Geometric Mean

TheoremChange of variables to polar co-ordinates#

Mathlib states this as integral_comp_polarCoord_symm.

integral_comp_polarCoord_symm.{u_1} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E]
  (f : ℝ × ℝ → E) :
  ∫ (p : ℝ × ℝ) in polarCoord.target, p.1 • f (↑polarCoord.symm p) = ∫ (p : ℝ × ℝ), f p
Sources
Mathlibintegral_comp_polarCoord_symm
Uses 12
Statement usesBochner integral · Carathéodory's theorem (measure theory) · Inverse trigonometric functions · Lebesgue measure (Measures and integral calculus)
Proof usesChange of variables formula · Derivative at a point · Derivative of a composition of functions (Analysis) · Giry monad · Kernel of a linear map · Noetherian module · Product of vector spaces · Sum of subspaces

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.