curveIntegral_segment_source — Mathlib

English

If ω is continuous, then the derivative of the segment integral equals ω(a) at a.

Русский

Если ω непрерывна, то производная интеграла по сегменту равна ω(a) в точке a.

LaTeX

$$$\\text{HasFDerivAt}\\left(\\int_{\\text{segment } a..b} ω(x)dx, ω(a)\\right)\\text{ at } 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 on the whole space. -/
theorem curveIntegral_segment_source (hω : Continuous ω) : HasFDerivAt (∫ᶜ x in .segment a ·, ω x) (ω a) a :=
  .curveIntegral_segment_source' <| .of_forall fun _ ↦ hω.continuousAt

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