integral_hasFDerivWithinAt_of_tendsto_ae

English

Let f be interval-integrable on [a,b] and measurable along la, lb with appropriate tendsto to ca, cb; then HasFDerivWithinAt of F with derivative L holds.

Русский

Пусть f интегрируем на [a,b], измерим по соответствующим фильтрам и пределы ca, cb достигаются; тогда HasFDerivWithinAt имеет вид L.

LaTeX

$$$\\text{HasFDerivWithinAt}(F,L,s\\times t)\\; (a,b).$$$

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 • cb - u • ca` 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 `ca`
and `cb` almost surely at the filters `la` and `lb` from the following table.

| `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_of_tendsto_ae (hf : IntervalIntegrable f volume a b) {s t : Set ℝ}
    [FTCFilter a (𝓝[s] a) la] [FTCFilter b (𝓝[t] b) lb] (hmeas_a : StronglyMeasurableAtFilter f la)
    (hmeas_b : StronglyMeasurableAtFilter f lb) (ha : Tendsto f (la ⊓ ae volume) (𝓝 ca))
    (hb : Tendsto f (lb ⊓ ae volume) (𝓝 cb)) :
    HasFDerivWithinAt (fun p : ℝ × ℝ => ∫ x in p.1..p.2, f x) ((snd ℝ ℝ ℝ).smulRight cb - (fst ℝ ℝ ℝ).smulRight ca)
      (s ×ˢ t) (a, b) :=
  by
  rw [HasFDerivWithinAt, nhdsWithin_prod_eq]
  have :=
    integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae hf hmeas_a hmeas_b ha hb
      (tendsto_const_pure.mono_right FTCFilter.pure_le : Tendsto _ _ (𝓝[s] a)) tendsto_fst
      (tendsto_const_pure.mono_right FTCFilter.pure_le : Tendsto _ _ (𝓝[t] b)) tendsto_snd
  refine .of_isLittleO <| (this.congr_left ?_).trans_isBigO ?_
  · simp [sub_smul]
  · exact isBigO_fst_prod.norm_left.add isBigO_snd_prod.norm_left

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