Integration

DefinitionRiemann sums#

The integral sum of f : ℝⁿ → E over a tagged prepartition π w.r.t. box-additive volume vol with codomain E →L[ℝ] F is the sum of vol J (f (π.tag J)) over all boxes of π.

BoxIntegral.integralSum.{u, v, w} {ι : Type u} {E : Type v} {F : Type w} [NormedAddCommGroup E]
  [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {I : BoxIntegral.Box ι}
  (f : (ι → ℝ) → E) (vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤)
  (π : BoxIntegral.TaggedPrepartition I) : F
Sources
MathlibBoxIntegral.integralSum
Uses 3 · Used by 1
Statement usesContinuous linear map · Finite set · Normed vector space over a normed field
Used byDivergence theorem

TheoremAntiderivative of a continuous function#

Fundamental theorem of calculus-1, derivative in the right endpoint.

If f : ℝ → E is continuous, then the derivative of u ↦ ∫ x in a..u, f x at b is f b.

Continuous.deriv_integral.{u_3} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E]
  [CompleteSpace E] (f : ℝ → E) (hf : Continuous f) (a b : ℝ) :
  deriv (fun u => ∫ (x : ℝ) in a..u, f x) b = f b
Sources
MathlibContinuous.deriv_integral
Uses 6
Statement usesBochner integral · Carathéodory's theorem (measure theory) · Differentials (linear tangent functions) · Lebesgue measure (Measures and integral calculus)
Proof usesDerivative at a point · Fundamental Theorem of Integral Calculus

TheoremChange of variable#

Change of variables, most common version. If f has continuous derivative f' on [a, b], and g is continuous, then we can substitute u = f x to get ∫ x in a..b, f' x • (g ∘ f) x = ∫ u in f a..f b, g u.

If the function f is monotone or antitone, see also integral_deriv_smul_comp_of_deriv_nonneg and integral_deriv_smul_comp_of_deriv_nonpos dropping all assumptions on g.

intervalIntegral.integral_deriv_smul_comp.{u_1} {a b : ℝ} {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℝ E] {f f' : ℝ → ℝ} {g : ℝ → E} (h : ∀ x ∈ Set.uIcc a b, HasDerivAt f (f' x) x)
  (h' : ContinuousOn f' (Set.uIcc a b)) (hg : Continuous g) :
  ∫ (x : ℝ) in a..b, f' x • (g ∘ f) x = ∫ (x : ℝ) in f a..f b, g x
Sources
MathlibintervalIntegral.integral_deriv_smul_comp
Uses 7 · Used by 1
Statement usesBochner integral · Carathéodory's theorem (measure theory) · Derivative at a point · Lebesgue measure (Measures and integral calculus) · Topological ring
Proof usesFundamental theorem of calculus, part 2 · Image of a segment
Used byLévy continuity theorem

TheoremIntegration by parts#

Integration by parts. Special case of intervalIntegrable.integral_mul_deriv_eq_deriv_mul_of_hasDeriv_right where the functions have a derivative also at the endpoints. For improper integrals, see MeasureTheory.integral_mul_deriv_eq_deriv_mul, MeasureTheory.integral_Ioi_mul_deriv_eq_deriv_mul, and MeasureTheory.integral_Iic_mul_deriv_eq_deriv_mul.

intervalIntegral.integral_mul_deriv_eq_deriv_mul.{u_1} {a b : ℝ} {A : Type u_1} [NormedRing A]
  [NormedAlgebra ℝ A] [CompleteSpace A] {u v u' v' : ℝ → A}
  (hu : ∀ x ∈ Set.uIcc a b, HasDerivAt u (u' x) x) (hv : ∀ x ∈ Set.uIcc a b, HasDerivAt v (v' x) x)
  (hu' : IntervalIntegrable u' MeasureTheory.volume a b)
  (hv' : IntervalIntegrable v' MeasureTheory.volume a b) :
  ∫ (x : ℝ) in a..b, u x * v' x = u b * v b - u a * v a - ∫ (x : ℝ) in a..b, u' x * v x
Sources
MathlibintervalIntegral.integral_mul_deriv_eq_deriv_mul
Uses 5
Statement usesBochner integral · Carathéodory's theorem (measure theory) · Derivative at a point · Lebesgue measure (Measures and integral calculus)
Proof usesFundamental theorem of calculus, part 2

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.