Contributing FTC-2 for Banach spaces

Stream: mathlib4

[Victor Liu]

Hi there! I've concluded a proof for the fundamental theorem of calculus part 2 / mean value theorem for functions with values in a Banach space. I have read the contributing guidelines, and the source code at its current stage is in this file.

I'll be naming my branch victorliu5296/mean-value-banach.

import Mathlib.Topology.MetricSpace.Basic
import Mathlib.Analysis.NormedSpace.Basic
import Mathlib.Analysis.Calculus.FDeriv.Basic
import Mathlib.MeasureTheory.Integral.IntervalIntegral
import Mathlib.MeasureTheory.Integral.FundThmCalculus

open Set Function Topology Metric ContinuousLinearMap Filter Units MeasureTheory

section MeanValueBanach

/-- **Fundamental theorem of calculus-2** or **Mean Value Theorem** for Banach spaces: If `f : X → Y` is differentiable along the line segment
from `a` to `b`, then the change in `f` equals the integral of its derivative along this path. -/
lemma integral_eq_sub_of_hasFDerivAt
    {X Y : Type*} [NormedAddCommGroup X] [NormedSpace ℝ X]
    [NormedAddCommGroup Y] [NormedSpace ℝ Y] [CompleteSpace Y]
    {f : X → Y} {f' : X → X →L[ℝ] Y} {a b : X}
    (hcont : ContinuousOn (fun t : ℝ ↦
      (f' (a + t • (b - a)) : X →L[ℝ] Y)) (Set.Icc 0 1))
    (hderiv : ∀ t ∈ Set.Icc (0 : ℝ) 1,
      HasFDerivAt f (f' (a + t • (b - a)) : X →L[ℝ] Y) (a + t • (b - a))) :
    f b - f a = ∫ (t : ℝ) in (0:ℝ)..(1:ℝ),
      (f' (a + t • (b - a)) : X →L[ℝ] Y) (b - a) := by
  -- Step 1: Define the path from a to b
  let γ : ℝ → X := fun t ↦ a + t • (b - a)
  have γ_continuous (t : ℝ) : ContinuousWithinAt γ (Icc 0 1) t := by
    simp [γ]
    apply ContinuousWithinAt.add
    · exact continuousWithinAt_const
    · apply ContinuousWithinAt.smul
      · exact continuousWithinAt_id
      · exact continuousWithinAt_const
  have hint : IntervalIntegrable (fun t ↦ (f' (γ t)) (b - a))
      MeasureTheory.volume 0 1 := by
    apply ContinuousOn.intervalIntegrable
    simp only [γ]
    apply ContinuousOn.clm_apply
    · simp
      exact hcont
    · exact continuousOn_const
  have hderiv' : ∀ t ∈ Set.uIcc (0 : ℝ) 1,
      HasDerivAt (f ∘ γ) ((f' (γ t)) (b - a)) t := by
    intro t ht
    apply HasFDerivAt.comp_hasDerivAt
    · aesop
    · simpa [γ, neg_add_eq_sub] using ((hasDerivAt_const _ a).add
        ((hasDerivAt_id' t).smul_const (b - a)))
  have : ∫ (t : ℝ) in (0 : ℝ)..1, (f' (a + t • (b - a))) (b - a)
      = (f ∘ γ) 1 - (f ∘ γ) 0 := by
    apply intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le
    · exact zero_le_one' ℝ
    · intro x hx
      exact ContinuousAt.comp_continuousWithinAt
        (HasFDerivAt.continuousAt (hderiv x hx)) (γ_continuous x)
    · intro x hx
      dsimp [γ] at hderiv'
      dsimp [γ]
      have hx' : x ∈ uIcc 0 1 := by
        simp
        simp at hx
        constructor
        · linarith [hx.left]
        · linarith [hx.right]
      exact HasDerivAt.hasDerivWithinAt (hderiv' x hx')
    · exact hint
  have : ∫ (t : ℝ) in (0 : ℝ)..1, (f' (a + t • (b - a))) (b - a)
    = f b - f a := by aesop
  exact _root_.id (Eq.symm this)

end MeanValueBanach

Since it is my first time contributing and the guide recommended to post progress while working on it, here is my current step-by-step plan on how to proceed:

1. Refine the proof with assistance of people here to follow the conventions and potentially make it more concise as it is pretty verbose at the moment.
2. Once confirmed that it is ready, I will place this as a theorem at the end of the FTC-2 section in the file Mathlib/MeasureTheory/Integral/FundThmCalculus.lean.
3. Seeing as this is part of an effort on formalizing the Newton-Kantorovich theorem for which I have largely used this reference:

@article{doi:10.1142/S0219530512500121,
author = {CIARLET, PHILIPPE G. and MARDARE, CRISTINEL},
title = {ON THE NEWTON–KANTOROVICH THEOREM},
journal = {Analysis and Applications},
volume = {10},
number = {03},
pages = {249-269},
year = {2012},
doi = {10.1142/S0219530512500121},

URL = {https://www.ljll.fr/mardare/recherche/pdf/NK_AA.pdf}
}

I plan on putting this at the end of docs/references.bib. At this stage, I have a question: does using the bibtool command require installing additional software or is it built-in?
bibtool --preserve.key.case=on --preserve.keys=on --pass.comments=on --print.use.tab=off -s -i docs/references.bib -o docs/references.bib

4. Create a pull request to merge my branch to master and resolve conflicts and whatnot at that stage.

[Kevin Buzzard]

Make the PR first, that's the way to get eyes on your code. If bibtool doesn't work for you then just do the best you can.

[Yury G. Kudryashov]

I suggest that you use docs#HasLineDerivAt or docs#HasLineDerivWithinAt

[Victor Liu]

Kevin Buzzard said:

Make the PR first, that's the way to get eyes on your code. If bibtool doesn't work for you then just do the best you can.

Right, turns out that the continuous integrations have a bot that will lint it for you

[Victor Liu]

Yury G. Kudryashov said:

I suggest that you use docs#HasLineDerivAt or docs#HasLineDerivWithinAt

Wait, for what?
The theorem statement in the paper really did explicitly use Fréchet derivatives and even went out of their way to define it themselves, so I used that since I'll need it for the proof of the Newton-Kantorovich theorem.
image.png

[Victor Liu]

Kevin Buzzard said:

Make the PR first, that's the way to get eyes on your code. If bibtool doesn't work for you then just do the best you can.

Here is the PR for reference:
https://github.com/leanprover-community/mathlib4/pull/15212

[Yury G. Kudryashov]

If you look at HasDerivAt that you use and unfold some definitions, you'll get HasLineDerivAt

[Victor Liu]

So if I'm getting this right, I have to replace HasDerivAt here with HasLineDerivAt?

  have hderiv' : ∀ t ∈ Set.uIcc (0 : ℝ) 1,
      HasDerivAt (f ∘ γ) ((f' (γ t)) (b - a)) t := by
    intro t ht
    apply HasFDerivAt.comp_hasDerivAt
    · aesop
    · simpa [γ, neg_add_eq_sub] using ((hasDerivAt_const _ a).add
        ((hasDerivAt_id' t).smul_const (b - a)))
  have : ∫ (t : ℝ) in (0 : ℝ)..1, (f' (a + t • (b - a))) (b - a)
      = (f ∘ γ) 1 - (f ∘ γ) 0 := by
    apply intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le
    · exact zero_le_one' ℝ
    · intro x hx
      exact ContinuousAt.comp_continuousWithinAt
        (HasFDerivAt.continuousAt (hderiv x hx)) (γ_continuous x)
    · intro x hx
      dsimp [γ] at hderiv'
      dsimp [γ]
      have hx' : x ∈ uIcc 0 1 := by
        simp only [zero_le_one, uIcc_of_le, mem_Icc]
        simp only [mem_Ioo] at hx
        constructor
        · linarith [hx.left]
        · linarith [hx.right]
      exact HasDerivAt.hasDerivWithinAt (hderiv' x hx')
    · exact hint

[Victor Liu]

I have a question, is it necessary to make this change? Because it seems like the moment I change it Lean throws a bunch of type errors

      HasLineDerivAt (f ∘ γ) ((f' (γ t)) (b - a)) t := by

application type mismatch
  @HasLineDerivAt (f ∘ γ)
argument
  f ∘ γ
has type
  ℝ → Y : Type u_2
but is expected to have type
  Type ?u.21446 : Type (?u.21446 + 1)

[Victor Liu]

And the current implementation seems to work just fine

[Yury G. Kudryashov]

Please read the definition of docs#HasLineDerivAt

[Yury G. Kudryashov]

You can write ∀ t ∈ Icc (0 : ℝ) 1, HasLineDerivAt ℝ f (f' t) (AffineMap.lineMap a b t) (b - a)

[Yury G. Kudryashov]

And use f' : ℝ → Y. BTW, why do you want f' to be continuous? Integrability is enough.