locallyIntegrable_finset_sum' — Mathlib

English

If f is locally integrable and g is a continuous function with compact support, then the product g • f is integrable.

Русский

Если f локально интегрируема и g непрерывна с компактной опорой, то произведение g • f интегрируемо.

LaTeX

$$$\operatorname{LocallyIntegrable}(f, \mu) \land \operatorname{Continuous}(g) \land \operatorname{HasCompactSupport}(g) \Rightarrow \operatorname{Integrable}(x \mapsto g(x) \cdot f(x), \mu)$$$

Lean4

theorem locallyIntegrable_finset_sum' {ι} (s : Finset ι) {f : ι → X → ε'''} (hf : ∀ i ∈ s, LocallyIntegrable (f i) μ) :
    LocallyIntegrable (∑ i ∈ s, f i) μ :=
  Finset.sum_induction f (fun g => LocallyIntegrable g μ) (fun _ _ => LocallyIntegrable.add) locallyIntegrable_zero hf

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