to_subbox_aux — Mathlib

English

If f is Integrable on I, then it is Integrable on any subbox J ≤ I.

Русский

Если f интегрируем на I, то она интегрируема и на любой подплощадке J ≤ I.

LaTeX

$$$\text{Integrable } I l f vol \rightarrow \text{Box.instLE.le } J I \rightarrow \text{Integrable } J l f vol$$$

Lean4

theorem to_subbox_aux (h : Integrable I l f vol) (hJ : J ≤ I) :
    ∃ y : F,
      HasIntegral J l f vol y ∧ Tendsto (integralSum f vol) (l.toFilteriUnion I (Prepartition.single I J hJ)) (𝓝 y) :=
  by
  refine
    (cauchy_map_iff_exists_tendsto.1 (h.cauchy_map_integralSum_toFilteriUnion (.single I J hJ))).imp fun y hy ↦ ⟨?_, hy⟩
  convert
    hy.comp
      (l.tendsto_embedBox_toFilteriUnion_top hJ) -- faster than `exact` here

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