English
For a scalar c, the Holder norm scales with the absolute value of c: eHolderNorm r (c • f) = |c|₊ · eHolderNorm r f.
Русский
Для скаляра c норма Холдера изменяется пропорционально |c|: eHolderNorm r (c • f) = |c|₊ · eHolderNorm r f.
LaTeX
$$$eHolderNorm\, r\; (c \cdot f) = \lVert c \rVert_{+} \cdot eHolderNorm\, r\; f$$$
Lean4
theorem eHolderNorm_smul {α} [NormedRing α] [Module α Y] [NormSMulClass α Y] (c : α) :
eHolderNorm r (c • f) = ‖c‖₊ * eHolderNorm r f :=
by
by_cases hc : ‖c‖₊ = 0
· rw [nnnorm_eq_zero] at hc
simp [hc]
by_cases hf : MemHolder r f
· refine le_antisymm ((hf.holderWith.smul c).eHolderNorm_le.trans ?_) <| mul_le_of_le_div' ?_
· rw [coe_mul, hf.coe_nnHolderNorm_eq_eHolderNorm, mul_comm]
· rw [← (hf.holderWith.smul c).memHolder.coe_nnHolderNorm_eq_eHolderNorm, ← coe_div hc]
refine HolderWith.eHolderNorm_le fun x₁ x₂ => ?_
rw [coe_div hc, ← ENNReal.mul_div_right_comm,
ENNReal.le_div_iff_mul_le (Or.inl <| coe_ne_zero.2 hc) <| Or.inl coe_ne_top, mul_comm, ← smul_eq_mul, ←
ENNReal.smul_def, ← edist_smul₀, ← Pi.smul_apply, ← Pi.smul_apply]
exact hf.smul.holderWith x₁ x₂
· rw [← eHolderNorm_eq_top] at hf
rw [hf, mul_top <| coe_ne_zero.2 hc, eHolderNorm_eq_top, MemHolder.smul_iff hc]
rw [nnnorm_eq_zero] at hc
intro h
exact h.eHolderNorm_lt_top.ne hf
