curveIntegral_segment_source — Mathlib

English

If hs is convex and hω is continuous on s, then HasFDerivWithinAt of the segment integral with derivative ω(a) at a ∈ s.

Русский

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

LaTeX

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

Lean4

/-- The integral of `ω` along `[a -[ℝ] b]`, as a function of `b`, has derivative `ω a` at `b = a`.
This is a `HasFDerivWithinAt` version assuming that `ω` is continuous on `s`. -/
theorem curveIntegral_segment_source (hs : Convex ℝ s) (hω : ContinuousOn ω s) (ha : a ∈ s) :
    HasFDerivWithinAt (∫ᶜ x in .segment a ·, ω x) (ω a) s a :=
  .curveIntegral_segment_source' hs (mem_of_superset self_mem_nhdsWithin hω) ha

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