smul_enorm — Mathlib

English

If c acts boundedly on ε and f: α → ε has finite integral, then c • f has finite integral.

Русский

Если элемент 𝕜 действует ограниченно на ε и f: α → ε имеет конечный интеграл, то c • f тоже имеет конечный интеграл.

LaTeX

$$$HasFiniteIntegral f μ \Rightarrow HasFiniteIntegral (c \cdot f) μ$$$

Lean4

@[fun_prop]
theorem smul_enorm [NormedAddGroup 𝕜] [SMul 𝕜 ε''] [ENormSMulClass 𝕜 ε''] (c : 𝕜) {f : α → ε''}
    (hf : HasFiniteIntegral f μ) : HasFiniteIntegral (c • f) μ :=
  by
  simp only [HasFiniteIntegral]
  calc
    ∫⁻ a : α, ‖c • f a‖ₑ ∂μ = ∫⁻ a : α, ‖c‖ₑ * ‖f a‖ₑ ∂μ := lintegral_congr fun i ↦ enorm_smul _ _
    _ < ∞ := by
      rw [lintegral_const_mul']
      exacts [mul_lt_top coe_lt_top hf, coe_ne_top]

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