smul — Mathlib

English

For counting measure, HasFiniteIntegral f count ⇔ tsum (‖f‖) < ∞.

Русский

Для счетной меры HasFiniteIntegral f count эквивалентно tsum (‖f‖) < ∞.

LaTeX

$$$HasFiniteIntegral f\;\text{Count} \iff tsum (\|f\|) < \infty$$$

Lean4

@[fun_prop]
theorem smul [NormedAddCommGroup 𝕜] [SMulZeroClass 𝕜 β] [IsBoundedSMul 𝕜 β] (c : 𝕜) {f : α → β}
    (hf : HasFiniteIntegral f μ) : HasFiniteIntegral (c • f) μ :=
  by
  simp only [HasFiniteIntegral]
  calc
    ∫⁻ a : α, ‖c • f a‖ₑ ∂μ ≤ ∫⁻ a : α, ‖c‖ₑ * ‖f a‖ₑ ∂μ := lintegral_mono fun i ↦ enorm_smul_le
    _ < ∞ := by
      rw [lintegral_const_mul']
      exacts [mul_lt_top coe_lt_top hf, coe_ne_top]
        -- TODO: weaken the hypothesis to a version of `ENormSMulClass` with `≤`,
        -- once such a typeclass exists.
        -- This will let us unify with `HasFiniteIntegral.smul` above.

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