integral_hasDerivWithinAt_right — Mathlib

English

If f is integrable on [a,b] and continuous at b, then HasDerivWithinAt for the right endpoint map exists with derivative f(b).

Русский

Если f интегрируема на [a,b] и непрерывна в b, то у нас есть производная по правому концу, равная f(b).

LaTeX

$$$\\text{HasDerivWithinAt}(u\\mapsto \\int_{a}^{u} f(x)dx, f(b), b).$$$

Lean4

/-- Fundamental theorem of calculus: if `f : ℝ → E` is integrable on `a..b` and `f x` is continuous
from the left or from the right at `b`, then `u ↦ ∫ x in a..u, f x` has left (resp., right)
derivative `f b` at `b`. -/
theorem integral_hasDerivWithinAt_right (hf : IntervalIntegrable f volume a b) {s t : Set ℝ}
    [FTCFilter b (𝓝[s] b) (𝓝[t] b)] (hmeas : StronglyMeasurableAtFilter f (𝓝[t] b)) (hb : ContinuousWithinAt f t b) :
    HasDerivWithinAt (fun u => ∫ x in a..u, f x) (f b) s b :=
  integral_hasDerivWithinAt_of_tendsto_ae_right hf hmeas (hb.mono_left inf_le_left)

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