English
If a is a nonzero element with respect to the norm, then HölderWith for a·f is equivalent to HölderWith for f (up to a computable scaling).
Русский
Если ‖a‖ ≠ 0, то HolderWith для a·f эквивалентен HolderWith для f (с учётом масштаба).
LaTeX
$$$\forall a, \; \|a\|_+ \neq 0 \Rightarrow \operatorname{HolderWith}\big(C \cdot \|a\|_+, r, a\cdot f\big) \iff \operatorname{HolderWith}(C,r,f)$$$
Lean4
theorem smul_iff {α} [SeminormedRing α] [Module α Y] [NormSMulClass α Y] (a : α) (ha : ‖a‖₊ ≠ 0) :
HolderWith (C * ‖a‖₊) r (a • f) ↔ HolderWith C r f := by
simp_rw [HolderWith, coe_mul, Pi.smul_apply, edist_smul₀, ENNReal.smul_def, smul_eq_mul, mul_comm (C : ℝ≥0∞),
mul_assoc, ENNReal.mul_le_mul_left (ENNReal.coe_ne_zero.mpr ha) ENNReal.coe_ne_top, mul_comm]
