Calculus along absolutely continuous curves

Mathlib's AbsolutelyContinuousOnInterval.integral_deriv_eq_sub is the fundamental theorem of calculus for an absolutely continuous real function. This file composes it with a C¹ function: if γ : ℝ → F is an absolutely continuous curve in a normed space with derivative V t at almost every time and φ : F → ℝ is C¹, then ∫_a^b φ'(γ t) (V t) dt = φ (γ b) - φ (γ a). In finite dimension, it also extends Mathlib's real-valued derivative integrability and fundamental-theorem results to curves.

Main results

• AbsolutelyContinuousOnInterval.integral_fderiv_apply_eq_sub: the fundamental theorem of calculus for the composition of a C¹ function with an absolutely continuous curve.
• AbsolutelyContinuousOnInterval.intervalIntegrable_of_ae_hasDerivAt: the almost-everywhere derivative of an absolutely continuous curve in a finite-dimensional space is interval integrable.
• AbsolutelyContinuousOnInterval.integral_eq_sub_of_ae_hasDerivAt: the fundamental theorem for the almost-everywhere derivative of an absolutely continuous curve in finite dimension.
• AbsolutelyContinuousOnInterval.intervalIntegrable_deriv_of_finiteDimensional and AbsolutelyContinuousOnInterval.integral_deriv_eq_sub_of_finiteDimensional: integrability and the fundamental theorem for the canonical derivative of such a curve.
• AbsolutelyContinuousOnInterval.integral_mul_deriv_eq_deriv_mul_of_ae_hasDerivAt: integration by parts with supplied almost-everywhere derivatives.
• AbsolutelyContinuousOnInterval.integral_div_eq_log_sub_log: the fundamental theorem for the logarithmic derivative of a nonvanishing absolutely continuous real function.
• TauCeti.Probability.survival_eq_exp_integral_hazard: a positive absolutely continuous survival function is reconstructed from its hazard rate.
• ContinuousOn.absolutelyContinuousOnInterval_of_hasDerivAt_off_countable: a continuous curve with an integrable derivative off a countable set is absolutely continuous.
• IntervalIntegrable.absolutelyContinuousOnInterval_intervalIntegral': indefinite integrals with base point in the integrability interval are absolutely continuous in any real normed space.

theorem AbsolutelyContinuousOnInterval.integral_fderiv_apply_eq_sub {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {γ V : ℝ → F} {a b : ℝ} (hγ : AbsolutelyContinuousOnInterval γ a b) (hV : ∀ᵐ (t : ℝ), t ∈ Set.uIoc a b → HasDerivAt γ (V t) t) {φ : F → ℝ} (hφ : ContDiff ℝ 1 φ) : ∫ (t : ℝ) in a..b, (fderiv ℝ φ (γ t)) (V t) = φ (γ b) - φ (γ a)

Fundamental theorem of calculus along an absolutely continuous curve: if γ is absolutely continuous on uIcc a b with derivative V t at almost every t ∈ uIoc a b and φ is C¹, then ∫ t in a..b, fderiv ℝ φ (γ t) (V t) = φ (γ b) - φ (γ a). The composition φ ∘ γ is absolutely continuous because φ is Lipschitz on the compact image γ '' uIcc a b.

theorem AbsolutelyContinuousOnInterval.intervalIntegrable_of_ae_hasDerivAt {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {γ V : ℝ → F} {a b : ℝ} [FiniteDimensional ℝ F] (hγ : AbsolutelyContinuousOnInterval γ a b) (hV : ∀ᵐ (t : ℝ), t ∈ Set.uIoc a b → HasDerivAt γ (V t) t) : IntervalIntegrable V MeasureTheory.volume a b

The almost-everywhere derivative V of a curve γ which is absolutely continuous on uIcc a b in a finite-dimensional real normed space is interval integrable on a..b. This reduces to Mathlib's real-valued AbsolutelyContinuousOnInterval.intervalIntegrable_deriv in the coordinates of a basis.

theorem AbsolutelyContinuousOnInterval.intervalIntegrable_deriv_of_finiteDimensional {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {γ : ℝ → F} {a b : ℝ} [FiniteDimensional ℝ F] (hγ : AbsolutelyContinuousOnInterval γ a b) : IntervalIntegrable (deriv γ) MeasureTheory.volume a b

The derivative of an absolutely continuous curve in a finite-dimensional real normed space is interval integrable.

theorem AbsolutelyContinuousOnInterval.integral_eq_sub_of_ae_hasDerivAt {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {γ V : ℝ → F} {a b : ℝ} [FiniteDimensional ℝ F] (hγ : AbsolutelyContinuousOnInterval γ a b) (hV : ∀ᵐ (t : ℝ), t ∈ Set.uIoc a b → HasDerivAt γ (V t) t) : ∫ (t : ℝ) in a..b, V t = γ b - γ a

The fundamental theorem of calculus for the almost-everywhere derivative of an absolutely continuous curve in a finite-dimensional real normed space.

theorem AbsolutelyContinuousOnInterval.integral_deriv_eq_sub_of_finiteDimensional {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {γ : ℝ → F} {a b : ℝ} [FiniteDimensional ℝ F] (hγ : AbsolutelyContinuousOnInterval γ a b) : ∫ (t : ℝ) in a..b, deriv γ t = γ b - γ a

The fundamental theorem of calculus for an absolutely continuous curve in a finite-dimensional real normed space.

theorem AbsolutelyContinuousOnInterval.norm_sub_le_integral_norm_deriv_sub {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {γ : ℝ → F} {a b : ℝ} [FiniteDimensional ℝ F] {p : ℝ → F} (hp : AbsolutelyContinuousOnInterval p a b) (hγ : AbsolutelyContinuousOnInterval γ a b) (ha : p a = γ a) {t : ℝ} (ht : t ∈ Set.Icc a b) : ‖p t - γ t‖ ≤ ∫ (v : ℝ) in a..b, ‖deriv p v - deriv γ v‖

For two absolutely continuous curves with the same left endpoint, their pointwise distance is bounded by the L¹ difference of their velocities over the whole interval.

theorem AbsolutelyContinuousOnInterval.aemeasurable_restrict_Ioc {F : Type u_1} [NormedAddCommGroup F] {γ : ℝ → F} {a b : ℝ} [MeasurableSpace F] [BorelSpace F] (hγ : AbsolutelyContinuousOnInterval γ a b) (hab : a ≤ b) : AEMeasurable γ (MeasureTheory.volume.restrict (Set.Ioc a b))

An AC curve is almost everywhere measurable on the ordered half-open parameter interval.

theorem AbsolutelyContinuousOnInterval.integrableOn_deriv_Ioc {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {γ : ℝ → F} {a b : ℝ} [FiniteDimensional ℝ F] (hγ : AbsolutelyContinuousOnInterval γ a b) (hab : a ≤ b) : MeasureTheory.IntegrableOn (deriv γ) (Set.Ioc a b) MeasureTheory.volume

The derivative of a finite-dimensional AC curve is integrable on the ordered half-open parameter interval.

theorem AbsolutelyContinuousOnInterval.integral_mul_deriv_eq_deriv_mul_of_ae_hasDerivAt {A : Type u_1} [NormedRing A] [NormedAlgebra ℝ A] [FiniteDimensional ℝ A] {f f' g g' : ℝ → A} {a b : ℝ} (hf : AbsolutelyContinuousOnInterval f a b) (hg : AbsolutelyContinuousOnInterval g a b) (hff' : ∀ᵐ (t : ℝ), t ∈ Set.uIoc a b → HasDerivAt f (f' t) t) (hgg' : ∀ᵐ (t : ℝ), t ∈ Set.uIoc a b → HasDerivAt g (g' t) t) : ∫ (t : ℝ) in a..b, f t * g' t = f b * g b - f a * g a - ∫ (t : ℝ) in a..b, f' t * g t

Integration by parts for absolutely continuous functions valued in a finite-dimensional real normed ring. The derivatives may be supplied only almost everywhere.

theorem AbsolutelyContinuousOnInterval.intervalIntegrable_div_of_ae_hasDerivAt {f V : ℝ → ℝ} {a b : ℝ} (hf : AbsolutelyContinuousOnInterval f a b) (h0 : ∀ t ∈ Set.uIcc a b, f t ≠ 0) (hV : ∀ᵐ (t : ℝ), t ∈ Set.uIoc a b → HasDerivAt f (V t) t) : IntervalIntegrable (fun (t : ℝ) => V t / f t) MeasureTheory.volume a b

The logarithmic derivative V / f of an absolutely continuous real function f that does not vanish on the interval is interval integrable, where V is the derivative of f at almost every point.

theorem AbsolutelyContinuousOnInterval.integral_div_eq_log_sub_log {f V : ℝ → ℝ} {a b : ℝ} (hf : AbsolutelyContinuousOnInterval f a b) (h0 : ∀ t ∈ Set.uIcc a b, f t ≠ 0) (hV : ∀ᵐ (t : ℝ), t ∈ Set.uIoc a b → HasDerivAt f (V t) t) : ∫ (t : ℝ) in a..b, V t / f t = Real.log (f b) - Real.log (f a)

The fundamental theorem of calculus for the logarithmic derivative: if f is absolutely continuous and nonvanishing on the interval, with derivative V at almost every point, then ∫ t in a..b, V t / f t = log (f b) - log (f a).

theorem TauCeti.Probability.survival_eq_exp_integral_hazard {f : ℝ → ℝ} {a x : ℝ} {S : ℝ → ℝ} (hS : AbsolutelyContinuousOnInterval S a x) (hpos : ∀ t ∈ Set.uIcc a x, 0 < S t) (hderiv : ∀ᵐ (t : ℝ), t ∈ Set.uIoc a x → HasDerivAt S (-f t) t) : IntervalIntegrable (fun (t : ℝ) => f t / S t) MeasureTheory.volume a x ∧ S x = S a * Real.exp (-∫ (t : ℝ) in a..x, f t / S t)

Survival reconstruction from the hazard rate. If S is absolutely continuous on the interval between a and x, is positive there, and has derivative -f almost everywhere, then the hazard rate f / S is interval integrable and S x = S a * exp (-∫ t in a..x, f t / S t).

theorem IntervalIntegrable.absolutelyContinuousOnInterval_intervalIntegral' {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : ℝ → F} {a b c : ℝ} (hf : IntervalIntegrable f MeasureTheory.volume a b) (hc : c ∈ Set.uIcc a b) : AbsolutelyContinuousOnInterval (fun (t : ℝ) => ∫ (v : ℝ) in c..t, f v) a b

An indefinite interval integral in a real normed space is absolutely continuous on its integrability interval, provided its base point belongs to that interval.

theorem ContinuousOn.absolutelyContinuousOnInterval_of_hasDerivAt_off_countable {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {f f' : ℝ → F} {a b : ℝ} {s : Set ℝ} (hf : ContinuousOn f (Set.uIcc a b)) (hs : s.Countable) (hd : ∀ t ∈ Set.Ioo (min a b) (max a b) \ s, HasDerivAt f (f' t) t) (hi : IntervalIntegrable f' MeasureTheory.volume a b) : AbsolutelyContinuousOnInterval f a b

A continuous curve with an integrable derivative outside a countable exceptional set is absolutely continuous on its parameter interval.