curveIntegral_segment_source' — Mathlib

English

If ω is continuous near a, then HasFDerivAt for the map b ↦ ∫_{segment a..b} ω(x) dx at b = a holds with derivative ω(a).

Русский

Если ω непрерывна около a, то производная в точке b = a для функции b ↦ ∫_{segment a..b} ω(x)dx равна ω(a).

LaTeX

$$$\\text{HasFDerivAt}\\left(\\int_{\\text{segment } a..b} ω(x)dx, ω(a)\\right)\\Big|_{b=a}$$$

Lean4

/-- The integral of `ω` along `[a -[ℝ] b]`, as a function of `b`, has derivative `ω a` at `b = a`.
This is a `HasFDerivAt` version assuming that `ω` is continuous in a neighborhood of `a`. -/
theorem curveIntegral_segment_source' (hω : ∀ᶠ z in 𝓝 a, ContinuousAt ω z) :
    HasFDerivAt (∫ᶜ x in .segment a ·, ω x) (ω a) a :=
  HasFDerivWithinAt.curveIntegral_segment_source' convex_univ (by simpa only [nhdsWithin_univ, continuousWithinAt_univ])
      (mem_univ _) |>.hasFDerivAt_of_univ

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