English
Variant with 𝕜-valued functions: rescale the unit interval to obtain a derivative relation: z1 times the integral of f' under the affine map equals difference f(z0+z1)−f(z0).
Русский
Вариант для функций, значимых в 𝕜: при преобразовании единичного интервала получаем отношение для производной; разность значений функции компенсирует интеграл.
LaTeX
$$$ z_1 \\int_{0}^{1} f'(z_0 + t z_1) dt = f(z_0+z_1) - f(z_0) $$$
Lean4
/-- A variant of `intervalIntegral.integral_deriv_eq_sub`, the Fundamental theorem
of calculus, involving integrating over the unit interval. -/
theorem integral_unitInterval_deriv_eq_sub [RCLike 𝕜] [NormedSpace 𝕜 E] [IsScalarTower ℝ 𝕜 E] {f f' : 𝕜 → E} {z₀ z₁ : 𝕜}
(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₀ :=
by
let γ (t : ℝ) : 𝕜 := z₀ + t • z₁
have hint : IntervalIntegrable (z₁ • (f' ∘ γ)) MeasureTheory.volume 0 1 :=
(ContinuousOn.const_smul hcont z₁).intervalIntegrable_of_Icc zero_le_one
have hderiv' (t) (ht : t ∈ Set.uIcc (0 : ℝ) 1) : HasDerivAt (f ∘ γ) (z₁ • (f' ∘ γ) t) t :=
by
refine (hderiv t <| (Set.uIcc_of_le (α := ℝ) zero_le_one).symm ▸ ht).scomp t <| .const_add _ ?_
simp [hasDerivAt_iff_isLittleO, sub_smul]
convert (integral_eq_sub_of_hasDerivAt hderiv' hint) using 1
· simp_rw [← integral_smul, Function.comp_apply, γ]
· simp only [γ, Function.comp_apply, one_smul, zero_smul, add_zero]
