integral_hasDerivWithinAt_of_tendsto_ae_left

English

If f is interval-integrable on [a,b] and f has finite ae-limit at a, then derivative of u ↦ ∫_{u}^{b} f(x) dx at a equals −c.

Русский

Если f интегрируема на [a,b] и имеет предел c ae при a, то производная u↦∫_{u}^{b} f(x) dx в a равна −c.

LaTeX

$$$\\text{deriv}_{a}(u\\mapsto \\int_{u}^{b} f(x)dx) = -c.$$$

Lean4

/-- Fundamental theorem of calculus: if `f : ℝ → E` is integrable on `a..b` and `f x` has a finite
limit `c` almost surely as `x` tends to `a` from the right or from the left,
then `u ↦ ∫ x in u..b, f x` has right (resp., left) derivative `-c` at `a`. -/
theorem integral_hasDerivWithinAt_of_tendsto_ae_left (hf : IntervalIntegrable f volume a b) {s t : Set ℝ}
    [FTCFilter a (𝓝[s] a) (𝓝[t] a)] (hmeas : StronglyMeasurableAtFilter f (𝓝[t] a))
    (ha : Tendsto f (𝓝[t] a ⊓ ae volume) (𝓝 c)) : HasDerivWithinAt (fun u => ∫ x in u..b, f x) (-c) s a :=
  by
  simp only [integral_symm b]
  exact (integral_hasDerivWithinAt_of_tendsto_ae_right hf.symm hmeas ha).neg

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