hasFiniteIntegral_smul_iff — Mathlib

English

For unit c in a normed ring, HasFiniteIntegral (c • f) μ ↔ HasFiniteIntegral f μ.

Русский

Для единицы c в нормированном кольце, HasFiniteIntegral (c • f) μ эквивалентно HasFiniteIntegral f μ.

LaTeX

$$$HasFiniteIntegral (instHSMul.hSMul c f) μ \iff HasFiniteIntegral f μ$$$

Lean4

theorem hasFiniteIntegral_smul_iff [NormedRing 𝕜] [MulActionWithZero 𝕜 β] [IsBoundedSMul 𝕜 β] {c : 𝕜} (hc : IsUnit c)
    (f : α → β) : HasFiniteIntegral (c • f) μ ↔ HasFiniteIntegral f μ :=
  by
  obtain ⟨c, rfl⟩ := hc
  constructor
  · intro h
    simpa only [smul_smul, Units.inv_mul, one_smul] using h.smul ((c⁻¹ : 𝕜ˣ) : 𝕜)
  exact HasFiniteIntegral.smul _

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