feat(measure_theory/interval_integral): FTC-2 (#4945)

The second fundamental theorem of calculus and supporting lemmas


Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

src/analysis/calculus/mean_value.lean

@@ -409,6 +409,57 @@ theorem norm_image_sub_le_of_norm_deriv_le_segment_01 {C : ℝ}
 by simpa only [sub_zero, mul_one]
   using norm_image_sub_le_of_norm_deriv_le_segment hf bound 1 (right_mem_Icc.2 zero_le_one)
 
+theorem constant_of_has_deriv_right_zero (hcont : continuous_on f (Icc a b))
+  (hderiv : ∀ x ∈ Ico a b, has_deriv_within_at f 0 (Ici x) x) :
+  ∀ x ∈ Icc a b, f x = f a :=
+by simpa only [zero_mul, norm_le_zero_iff, sub_eq_zero] using
+  λ x hx, norm_image_sub_le_of_norm_deriv_right_le_segment
+    hcont hderiv (λ y hy, by rw norm_le_zero_iff) x hx
+
+theorem constant_of_deriv_within_zero (hdiff : differentiable_on ℝ f (Icc a b))
+  (hderiv : ∀ x ∈ Ico a b, deriv_within f (Icc a b) x = 0) :
+  ∀ x ∈ Icc a b, f x = f a :=
+begin
+  have H : ∀ x ∈ Ico a b, ∥deriv_within f (Icc a b) x∥ ≤ 0 :=
+    by simpa only [norm_le_zero_iff] using λ x hx, hderiv x hx,
+  simpa only [zero_mul, norm_le_zero_iff, sub_eq_zero] using
+    λ x hx, norm_image_sub_le_of_norm_deriv_le_segment hdiff H x hx,
+end
+
+variables {f' g : ℝ → E}
+
+/-- If two continuous functions on `[a, b]` have the same right derivative and are equal at `a`,
+  then they are equal everywhere on `[a, b]`. -/
+theorem eq_of_has_deriv_right_eq
+  (derivf : ∀ x ∈ Ico a b, has_deriv_within_at f (f' x) (Ici x) x)
+  (derivg : ∀ x ∈ Ico a b, has_deriv_within_at g (f' x) (Ici x) x)
+  (fcont : continuous_on f (Icc a b)) (gcont : continuous_on g (Icc a b))
+  (hi : f a = g a) :
+  ∀ y ∈ Icc a b, f y = g y :=
+begin
+  simp only [← @sub_eq_zero _ _ (f _)] at hi ⊢,
+  exact hi ▸ constant_of_has_deriv_right_zero (fcont.sub gcont)
+    (λ y hy, by simpa only [sub_self] using (derivf y hy).sub (derivg y hy)),
+end
+
+/-- If two differentiable functions on `[a, b]` have the same derivative within `[a, b]` everywhere
+  on `[a, b)` and are equal at `a`, then they are equal everywhere on `[a, b]`. -/
+theorem eq_of_deriv_within_eq (fdiff : differentiable_on ℝ f (Icc a b))
+  (gdiff : differentiable_on ℝ g (Icc a b))
+  (hderiv : eq_on (deriv_within f (Icc a b)) (deriv_within g (Icc a b)) (Ico a b))
+  (hi : f a = g a) :
+  ∀ y ∈ Icc a b, f y = g y :=
+begin
+  have A : ∀ y ∈ Ico a b, has_deriv_within_at f (deriv_within f (Icc a b) y) (Ici y) y :=
+    λ y hy, (fdiff y (mem_Icc_of_Ico hy)).has_deriv_within_at.nhds_within
+      (Icc_mem_nhds_within_Ici hy),
+  have B : ∀ y ∈ Ico a b, has_deriv_within_at g (deriv_within g (Icc a b) y) (Ici y) y :=
+    λ y hy, (gdiff y (mem_Icc_of_Ico hy)).has_deriv_within_at.nhds_within
+      (Icc_mem_nhds_within_Ici hy),
+  exact eq_of_has_deriv_right_eq A (λ y hy, (hderiv hy).symm ▸ B y hy) fdiff.continuous_on
+    gdiff.continuous_on hi
+end
+
 end
 
 /-! ### Vector-valued functions `f : E → F` -/

src/measure_theory/interval_integral.lean

@@ -5,7 +5,8 @@ Author: Yury G. Kudryashov
 -/
 import measure_theory.set_integral
 import measure_theory.lebesgue_measure
-import analysis.calculus.deriv
+import analysis.calculus.fderiv_measurable
+import analysis.calculus.mean_value
 
 /-!
 # Integral over an interval
@@ -203,10 +204,14 @@ begin
   all_goals
   { refine measure_theory.integrable_on.mono_set _ Ioc_subset_Icc_self,
     refine continuous_on.integrable_on_compact compact_Icc hum (hu.mono _) },
-  { exact Icc_subset_interval },
-  { exact Icc_subset_interval' }
+  exacts [Icc_subset_interval, Icc_subset_interval']
 end
 
+lemma continuous_on.interval_integrable_of_Icc {u : ℝ → E} {a b : ℝ} (h : a ≤ b)
+  (hu : continuous_on u (Icc a b)) (hum : measurable u) :
+  interval_integrable u μ a b :=
+continuous_on.interval_integrable ((interval_of_le h).symm ▸ hu) hum
+
 /-- A continuous function on `ℝ` is `interval_integrable` with respect to any locally finite measure
 `ν` on ℝ. -/
 lemma continuous.interval_integrable [borel_space E] {u : ℝ → E} (hu : continuous u) (a b : ℝ) :
@@ -1214,4 +1219,90 @@ lemma deriv_within_integral_left (hf : interval_integrable f volume a b)
   deriv_within (λ u, ∫ x in u..b, f x) s a = -f a :=
 (integral_has_deriv_within_at_left hf ha).deriv_within hs
 
+
+/-~ ### Theorems pertaining to FTC-2. -/
+
+variables {f' : ℝ → E}
+
+/-- The integral of a continuous function is differentiable on a real set `s`. -/
+theorem differentiable_on_integral_of_continuous {s : set ℝ}
+  (hintg : ∀ x ∈ s, interval_integrable f volume a x) (hcont : continuous f) :
+  differentiable_on ℝ (λ u, ∫ x in a..u, f x) s :=
+λ y hy, (integral_has_deriv_at_right (hintg y hy)
+          hcont.continuous_at).differentiable_at.differentiable_within_at
+
+/-- The integral of a continuous function is continuous on a real set `s`. This is true even
+  without the assumption of continuity, but a proof of that fact does not yet exist in mathlib. -/
+theorem continuous_on_integral_of_continuous {s : set ℝ}
+  (hintg : ∀ x ∈ s, interval_integrable f volume a x) (hcont : continuous f) :
+  continuous_on (λ u, ∫ x in a..u, f x) s :=
+(differentiable_on_integral_of_continuous hintg hcont).continuous_on
+
+/-- Fundamental theorem of calculus-2: If `f : ℝ → E` is continuous on `[a, b]` and has a right
+  derivative at `f' x` for all `x` in `[a, b)`, and `f'` is continuous on `[a, b]` and measurable,
+  then `∫ y in a..b, f' y` equals `f b - f a`. -/
+theorem integral_eq_sub_of_has_deriv_right_of_le (hab : a ≤ b) (hcont : continuous_on f (Icc a b))
+  (hderiv : ∀ x ∈ Ico a b, has_deriv_within_at f (f' x) (Ici x) x)
+  (hcont' : continuous_on f' (Icc a b)) (hmeas' : measurable f') :
+  ∫ y in a..b, f' y = f b - f a :=
+begin
+  refine eq_sub_of_add_eq (eq_of_has_deriv_right_eq (λ y hy, _) hderiv
+    (λ y hy, _) hcont (by simp) _ (right_mem_Icc.2 hab)),
+  { refine (integral_has_deriv_within_at_right _ _).add_const _,
+    { refine (hcont'.mono _).interval_integrable hmeas',
+      simp [hy.1, Icc_subset_Icc_right hy.2.le] },
+    { exact (hcont' _ (mem_Icc_of_Ico hy)).mono_of_mem (Icc_mem_nhds_within_Ioi hy) } },
+  { -- TODO: prove that integral of any integrable function is continuous, and use here
+    letI : tendsto_Ixx_class Ioc (𝓟 (Icc a b)) (𝓟 (Ioc a b)) :=
+      tendsto_Ixx_class_principal.2 (λ x hx y hy, Ioc_subset_Ioc hx.1 hy.2),
+    haveI : is_measurably_generated (𝓝[Ioc a b] y) :=
+      is_measurable_Ioc.nhds_within_is_measurably_generated y,
+    letI : FTC_filter y (𝓝[Icc a b] y) (𝓝[Ioc a b] y) := ⟨pure_le_nhds_within hy, inf_le_left⟩,
+    refine (integral_has_deriv_within_at_right _ _).continuous_within_at.add
+      continuous_within_at_const,
+    { exact (hcont'.mono $ Icc_subset_Icc_right hy.2).interval_integrable_of_Icc hy.1 hmeas' },
+    { exact (hcont' y hy).mono Ioc_subset_Icc_self } }
+end
+
+/-- Fundamental theorem of calculus-2: If `f : ℝ → E` is continuous on `[a, b]` (where `a ≤ b`) and
+  has a right derivative at `f' x` for all `x` in `[a, b)`, and `f'` is continuous on `[a, b]` and
+  measurable, then `∫ y in a..b, f' y` equals `f b - f a`. -/
+theorem integral_eq_sub_of_has_deriv_right (hcont : continuous_on f (interval a b))
+  (hderiv : ∀ x ∈ Ico (min a b) (max a b), has_deriv_within_at f (f' x) (Ici x) x)
+  (hcont' : continuous_on f' (interval a b)) (hmeas' : measurable f') :
+  ∫ y in a..b, f' y = f b - f a :=
+begin
+  cases le_total a b with hab hab,
+  { simp only [interval_of_le, min_eq_left, max_eq_right, hab] at hcont hcont' hderiv,
+    exact integral_eq_sub_of_has_deriv_right_of_le hab hcont hderiv hcont' hmeas' },
+  { simp only [interval_of_ge, min_eq_right, max_eq_left, hab] at hcont hcont' hderiv,
+    rw [integral_symm, integral_eq_sub_of_has_deriv_right_of_le hab hcont hderiv hcont' hmeas',
+      neg_sub] }
+end
+
+/-- Fundamental theorem of calculus-2: If `f : ℝ → E` is continuous on `[a, b]` and has a derivative
+  at `f' x` for all `x` in `[a, b)`, and `f'` is continuous on `[a, b]` and measurable, then
+  `∫ y in a..b, f' y` equals `f b - f a`. -/
+theorem integral_eq_sub_of_has_deriv_at' (hcont : continuous_on f (interval a b))
+  (hderiv : ∀ x ∈ Ico (min a b) (max a b), has_deriv_at f (f' x) x)
+  (hcont' : continuous_on f' (interval a b)) (hmeas' : measurable f') :
+  ∫ y in a..b, f' y = f b - f a :=
+integral_eq_sub_of_has_deriv_right hcont (λ x hx, (hderiv x hx).has_deriv_within_at) hcont' hmeas'
+
+/-- Fundamental theorem of calculus-2: If `f : ℝ → E` has a derivative at `f' x` for all `x` in
+  `[a, b)` and `f'` is continuous on `[a, b]` and measurable, then `∫ y in a..b, f' y` equals
+  `f b - f a`. -/
+theorem integral_eq_sub_of_has_deriv_at (hderiv : ∀ x ∈ interval a b, has_deriv_at f (f' x) x)
+  (hcont' : continuous_on f' (interval a b)) (hmeas' : measurable f') :
+  ∫ y in a..b, f' y = f b - f a :=
+integral_eq_sub_of_has_deriv_at' (λ x hx, (hderiv x hx).continuous_at.continuous_within_at)
+  (λ x hx, hderiv _ (mem_Icc_of_Ico hx)) hcont' hmeas'
+
+/-- Fundamental theorem of calculus-2: If `f : ℝ → E` is differentiable at every `x` in `[a, b]` and
+  its derivative is continuous on `[a, b]`, then `∫ y in a..b, deriv f y` equals `f b - f a`. -/
+theorem integral_deriv_eq_sub (hderiv : ∀ x ∈ interval a b, differentiable_at ℝ f x)
+  (hcont' : continuous_on (deriv f) (interval a b)) :
+  ∫ y in a..b, deriv f y = f b - f a :=
+integral_eq_sub_of_has_deriv_at (λ x hx, (hderiv x hx).has_deriv_at) hcont' (measurable_deriv f)
+
 end interval_integral