eLpNorm'_const_smul — Mathlib

English

For q > 0, scaling the function scales the eLpNorm' by the modulus of the scalar: eLpNorm'(c f)_{q} = |c|_e · eLpNorm'(f)_{q}.

Русский

Для q > 0 однородность: eLpNorm'(c f)_{q} = |c|ₑ · eLpNorm'(f)_{q}.

LaTeX

$$$$eLpNorm'(c \\cdot f)_{q} \\\\;= \\\\; \\|c\\|_e \\, eLpNorm'(f)_{q} \qquad (q > 0).$$$$

Lean4

theorem eLpNorm'_const_smul {f : α → F} (c : 𝕜) (hq_pos : 0 < q) : eLpNorm' (c • f) q μ = ‖c‖ₑ * eLpNorm' f q μ :=
  by
  obtain rfl | hc := eq_or_ne c 0
  · simp [eLpNorm'_eq_lintegral_enorm, hq_pos]
  refine le_antisymm (eLpNorm'_const_smul_le hq_pos) <| ENNReal.mul_le_of_le_div' ?_
  simpa [enorm_inv, hc, ENNReal.div_eq_inv_mul] using eLpNorm'_const_smul_le (c := c⁻¹) (f := c • f) hq_pos

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