English
If f is interval-integrable on [a,b] and has finite ae-limits ca, cb at a and b, then the derivative of F is dF_{(a,b)}(h,k) = k cb − h ca.
Русский
Если f интегрируема на [a,b] и имеет пределы ca, cb, то производная F есть dF_{(a,b)}(h,k)=k cb−h ca.
LaTeX
$$$dF_{(a,b)}(h,k)=k c_b - h c_a.$$$
Lean4
/-- Let `f` be a measurable function integrable on `a..b`. The function `(u, v) ↦ ∫ x in u..v, f x`
has derivative `(u, v) ↦ v • f b - u • f a` within `s × t` at `(a, b)`, where
`s ∈ {Iic a, {a}, Ici a, univ}` and `t ∈ {Iic b, {b}, Ici b, univ}` provided that `f` tends to
`f a` and `f b` at the filters `la` and `lb` from the following table. In most cases this assumption
is definitionally equal `ContinuousAt f _` or `ContinuousWithinAt f _ _`.
| `s` | `la` | `t` | `lb` |
| ------- | ---- | --- | ---- |
| `Iic a` | `𝓝[≤] a` | `Iic b` | `𝓝[≤] b` |
| `Ici a` | `𝓝[>] a` | `Ici b` | `𝓝[>] b` |
| `{a}` | `⊥` | `{b}` | `⊥` |
| `univ` | `𝓝 a` | `univ` | `𝓝 b` |
-/
theorem integral_hasFDerivWithinAt (hf : IntervalIntegrable f volume a b) (hmeas_a : StronglyMeasurableAtFilter f la)
(hmeas_b : StronglyMeasurableAtFilter f lb) {s t : Set ℝ} [FTCFilter a (𝓝[s] a) la] [FTCFilter b (𝓝[t] b) lb]
(ha : Tendsto f la (𝓝 <| f a)) (hb : Tendsto f lb (𝓝 <| f b)) :
HasFDerivWithinAt (fun p : ℝ × ℝ => ∫ x in p.1..p.2, f x)
((snd ℝ ℝ ℝ).smulRight (f b) - (fst ℝ ℝ ℝ).smulRight (f a)) (s ×ˢ t) (a, b) :=
integral_hasFDerivWithinAt_of_tendsto_ae hf hmeas_a hmeas_b (ha.mono_left inf_le_left) (hb.mono_left inf_le_left)
