Fundamental theorem of calculus and integration by parts for absolutely continuous functions

This file proves that:

• AbsolutelyContinuousOnInterval.integral_deriv_eq_sub: If f is absolutely continuous on uIcc a b, then Fundamental Theorem of Calculus holds for f' on a..b, i.e. ∫ (x : ℝ) in a..b, deriv f x = f b - f a.
• AbsolutelyContinuousOnInterval.integral_mul_deriv_eq_deriv_mul: Integration by Parts holds for absolutely continuous functions, i.e. if f and g are absolutely continuous on uIcc a b, then ∫ x in a..b, f x * deriv g x = f b * g b - f a * g a - ∫ x in a..b, deriv f x * g x.

Tags

absolutely continuous, fundamental theorem of calculus, integration by parts

theorem exists_dist_slope_lt_pairwiseDisjoint_hasSum {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {f f' : ℝ → F} {d b η : ℝ} (hdb : d ≤ b) (hf : ∀ᵐ (x : ℝ), x ∈ Set.Ioo d b → HasDerivAt f (f' x) x) (hη : 0 < η) : ∃ (u : Set (ℝ × ℝ)), (∀ z ∈ u, (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) (f' z.1) < η) ∧ (u.PairwiseDisjoint fun (z : ℝ × ℝ) => Set.Icc z.1 z.2) ∧ HasSum (fun (z : ↑u) => (↑z).2 - (↑z).1) (b - d)

If f has derivative f' a.e. on [d, b] and η is positive, then there is a collection of pairwise disjoint closed subintervals of [a, b] of total length b - a where the slope of f on each subinterval [x, y] differs from f' x by at most η.

theorem AbsolutelyContinuousOnInterval.dist_le_of_pairwiseDisjoint_hasSum {X : Type u_1} [PseudoMetricSpace X] {f : ℝ → X} {d b y : ℝ} (hdb : d ≤ b) (hf : AbsolutelyContinuousOnInterval f d b) {u : Set (ℝ × ℝ)} (hu₁ : ∀ z ∈ u, d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) (hu₂ : u.PairwiseDisjoint fun (z : ℝ × ℝ) => Set.Icc z.1 z.2) (hu₃ : HasSum (fun (z : ↑u) => (↑z).2 - (↑z).1) (b - d)) (hu₄ : HasSum (fun (z : ↑u) => dist (f (↑z).1) (f (↑z).2)) y) : dist (f d) (f b) ≤ y

If f is absolutely continuous on [d, b] and there is a collection of pairwise disjoint closed subintervals of (d, b) of total length b - d such that the sum of dist (f x) (f y) for [x, y] in the collection is equal to y, then dist (f b) (f d) ≤ y.

theorem AbsolutelyContinuousOnInterval.const_of_ae_hasDerivAt_zero {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : ℝ → F} {a b : ℝ} (hf : AbsolutelyContinuousOnInterval f a b) (hf₀ : ∀ᵐ (x : ℝ), x ∈ Set.uIcc a b → HasDerivAt f 0 x) : ∃ (C : F), ∀ x ∈ Set.uIcc a b, f x = C

If f is absolutely continuous on uIcc a b and f' x = 0 for a.e. x ∈ uIcc a b, then f is constant on uIcc a b.

theorem AbsolutelyContinuousOnInterval.integral_deriv_eq_sub {f : ℝ → ℝ} {a b : ℝ} (hf : AbsolutelyContinuousOnInterval f a b) : ∫ (x : ℝ) in a..b, deriv f x = f b - f a

Fundamental Theorem of Calculus for absolutely continuous functions: if f is absolutely continuous on uIcc a b, then ∫ (x : ℝ) in a..b, deriv f x = f b - f a.

theorem AbsolutelyContinuousOnInterval.integral_deriv_mul_eq_sub {f g : ℝ → ℝ} {a b : ℝ} (hf : AbsolutelyContinuousOnInterval f a b) (hg : AbsolutelyContinuousOnInterval g a b) : ∫ (x : ℝ) in a..b, deriv f x * g x + f x * deriv g x = f b * g b - f a * g a

The integral of the derivative of a product of two absolutely continuous functions.

theorem AbsolutelyContinuousOnInterval.integral_mul_deriv_eq_deriv_mul {f g : ℝ → ℝ} {a b : ℝ} (hf : AbsolutelyContinuousOnInterval f a b) (hg : AbsolutelyContinuousOnInterval g a b) : ∫ (x : ℝ) in a..b, f x * deriv g x = f b * g b - f a * g a - ∫ (x : ℝ) in a..b, deriv f x * g x

Integration by parts for absolutely continuous functions.