integral_eq_of_hasDerivAt_off_countable_of_le

English

A refinement of the segment-derivative result under convexity assumptions.

Русский

Уточнение результата о производной по сегменту при предположении выпуклости.

LaTeX

$$$\\text{HasFDerivWithinAt}(\\int_{\\text{segment } a..·} ω(x)dx, ω(a), s, a)$$$

Lean4

/-- **Fundamental theorem of calculus, part 2**. This version assumes that `f` is continuous on the
interval and is differentiable off a countable set `s`.

See also

* `intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le` for a version that only assumes right
  differentiability of `f`;
* `MeasureTheory.integral_eq_of_hasDerivWithinAt_off_countable` for a version that works both
  for `a ≤ b` and `b ≤ a` at the expense of using unordered intervals instead of `Set.Icc`. -/
theorem integral_eq_of_hasDerivAt_off_countable_of_le [CompleteSpace E] (f f' : ℝ → E) {a b : ℝ} (hle : a ≤ b)
    {s : Set ℝ} (hs : s.Countable) (Hc : ContinuousOn f (Icc a b)) (Hd : ∀ x ∈ Ioo a b \ s, HasDerivAt f (f' x) x)
    (Hi : IntervalIntegrable f' volume a b) : ∫ x in a..b, f' x = f b - f a :=
  by
  set e : ℝ ≃L[ℝ] ℝ¹ := (ContinuousLinearEquiv.funUnique (Fin 1) ℝ ℝ).symm
  have e_symm : ∀ x, e.symm x = x 0 := fun x => rfl
  set F' : ℝ → ℝ →L[ℝ] E := fun x => smulRight (1 : ℝ →L[ℝ] ℝ) (f' x)
  have hF' : ∀ x y, F' x y = y • f' x := fun x y => rfl
  calc
    ∫ x in a..b, f' x = ∫ x in Icc a b, f' x := by
      rw [intervalIntegral.integral_of_le hle, setIntegral_congr_set Ioc_ae_eq_Icc]
    _ =
        ∑ i : Fin 1,
          ((∫ x in Icc (e a ∘ i.succAbove) (e b ∘ i.succAbove), f (e.symm <| i.insertNth (e b i) x)) -
            ∫ x in Icc (e a ∘ i.succAbove) (e b ∘ i.succAbove), f (e.symm <| i.insertNth (e a i) x)) :=
      by
      simp only [← interior_Icc] at Hd
      refine
        integral_divergence_of_hasFDerivAt_off_countable_of_equiv e ?_ ?_ (fun _ => f) (fun _ => F') s hs a b hle
          (fun _ => Hc) (fun x hx _ => Hd x hx) _ ?_ ?_
      · exact fun x y => (OrderIso.funUnique (Fin 1) ℝ).symm.le_iff_le
      · exact (volume_preserving_funUnique (Fin 1) ℝ).symm _
      · intro x; rw [Fin.sum_univ_one, hF', e_symm, Pi.single_eq_same, one_smul]
      · rw [intervalIntegrable_iff_integrableOn_Ioc_of_le hle] at Hi
        exact Hi.congr_set_ae Ioc_ae_eq_Icc.symm
    _ = f b - f a := by
      simp [e, Subsingleton.elim (const (Fin 0) _) isEmptyElim, volume_pi, Measure.pi_of_empty fun _ : Fin 0 ↦ _]

Похожие утверждения