Commit 2023-12-07 20:36 b5120c08

feat: add a version of FTC-2 with an integral over the unit interval (#8615) This adds the following version of the Fundamental Theorem of Calculus:

lemma integral_unitInterval_eq_sub {C E : Type*} [IsROrC C]
    [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedSpace C E]
    [CompleteSpace E] [IsScalarTower ℝ C E] {f f' : C → E} {z₀ z₁ : C}
    (hcont : ContinuousOn (fun t : ℝ ↦ f' (z₀ + t • z₁)) (Set.Icc 0 1))
    (hderiv : ∀ t ∈ Set.Icc (0 : ℝ) 1, HasDerivAt f (f' (z₀ + t • z₁)) (z₀ + t • z₁)) :
    z₁ • ∫ t in (0 : ℝ)..1, f' (z₀ + t • z₁) = f (z₀ + z₁) - f z₀ := ...

This is helpful for, e.g., estimating the complex logarithm.