The fundamental theorem of calculus for nonnegative derivatives

Mathlib's intervalIntegral.integral_eq_sub_of_hasDerivAt_of_le evaluates ∫ x in a..b, f x as F b - F a for an antiderivative F that is continuous on [a, b], provided f is interval integrable. When f is nonnegative on (a, b) the integrability is automatic (intervalIntegral.integrableOn_deriv_of_nonneg), which matters for integrands that are unbounded at an endpoint, such as 1 / √(x - a). This file records the combined statement.

In the converse direction, FTC-1 recovers the derivative of a T-periodic function x from the integral equation x(t) - x(0) = ∫₀ᵗ Y over a single period [0, T], when Y is continuous and T-periodic: periodicity propagates the equation to all of ℝ.

It also records that along a loop f (with f a = f b) the integral of B (f x) (f' x) for a continuous bilinear map B is unchanged by subtracting a constant from f, because ∫ f' = 0.

Main declarations

• TauCeti.intervalIntegral.integral_eq_sub_of_hasDerivAt_of_le_of_nonneg
• TauCeti.hasDerivAt_of_periodic_of_sub_eq_integral
• ContinuousLinearMap.intervalIntegral_apply_apply_eq_sub_const

theorem TauCeti.intervalIntegral.integral_eq_sub_of_hasDerivAt_of_le_of_nonneg {F f : ℝ → ℝ} {a b : ℝ} (hab : a ≤ b) (hF : ContinuousOn F (Set.Icc a b)) (hd : ∀ x ∈ Set.Ioo a b, HasDerivAt F (f x) x) (hf : ∀ x ∈ Set.Ioo a b, 0 ≤ f x) : ∫ (x : ℝ) in a..b, f x = F b - F a

FTC-2 for a nonnegative derivative. If F is continuous on [a, b] and has derivative f x ≥ 0 at every x ∈ (a, b), then ∫ x in a..b, f x = F b - F a; the integrability of f is a consequence rather than a hypothesis.

theorem TauCeti.hasDerivAt_of_periodic_of_sub_eq_integral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {x Y : ℝ → E} {T : ℝ} (hT : 0 < T) (hxper : Function.Periodic x T) (hY : Continuous Y) (hYper : Function.Periodic Y T) (hint : ∀ t ∈ Set.Icc 0 T, x t - x 0 = ∫ (τ : ℝ) in 0..t, Y τ) (t : ℝ) : HasDerivAt x (Y t) t

Periodic solutions of an integral equation. Let x and a continuous Y be T-periodic, with T > 0. If x t - x 0 = ∫₀ᵗ Y for every t ∈ [0, T], then x has derivative Y t at every t.

theorem ContinuousLinearMap.intervalIntegral_apply_apply_eq_sub_const {V : Type u_1} {G : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup G] [NormedSpace ℝ G] (B : V →L[ℝ] V →L[ℝ] G) {a b : ℝ} {f f' : ℝ → V} (hfc : ContinuousOn f (Set.uIcc a b)) (hf : ∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivAt f (f' x) x) (hfab : f a = f b) (hf'ii : IntervalIntegrable f' MeasureTheory.volume a b) (m : V) : ∫ (x : ℝ) in a..b, (B (f x)) (f' x) = ∫ (x : ℝ) in a..b, (B (f x - m)) (f' x)

Along a loop f (that is, f a = f b) continuous on [a, b] with derivative f' in the interior, subtracting a constant from the first argument does not change the integral of B (f x) (f' x), since ∫ f' = f b - f a = 0.