of_measure_le_smul — Mathlib

English

If μ' ≤ c·μ with c ≠ ∞ and c ≠ 0, then integrability is preserved between μ and μ'.

Русский

Если μ' ≤ c·μ с c ≠ ∞ и c ≠ 0, то интегрируемость сохраняется между μ и μ'.

LaTeX

$$$hc: c \\neq \\infty \\; \\&\\; μ' ≤ c·μ \\Rightarrow Integrable(f, μ') ⇔ Integrable(f, μ).$$$

Lean4

theorem of_measure_le_smul {ε} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {μ' : Measure α} {c : ℝ≥0∞} (hc : c ≠ ∞)
    (hμ'_le : μ' ≤ c • μ) {f : α → ε} (hf : Integrable f μ) : Integrable f μ' :=
  by
  rw [← memLp_one_iff_integrable] at hf ⊢
  exact hf.of_measure_le_smul hc hμ'_le

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