smul — Mathlib

English

If a is from a normed ring with bounded scalar action, then a·f is Hölder with constant C·‖a‖.

Русский

Если a из нормированного кольца, действующее скаляром на Y ограничено, то a·f Холдер с константой C·‖a‖.

LaTeX

$$$\text{(a, hf)}\Rightarrow \operatorname{HolderWith}\big(C\cdot \lVert a\rVert_+, r, a\cdot f\big)$$$

Lean4

theorem smul {α} [SeminormedAddCommGroup α] [SMulZeroClass α Y] [IsBoundedSMul α Y] (a : α) (hf : HolderWith C r f) :
    HolderWith (C * ‖a‖₊) r (a • f) := fun x₁ x₂ =>
  by
  refine edist_smul_le _ _ _ |>.trans ?_
  rw [coe_mul, ENNReal.smul_def, smul_eq_mul, mul_comm (C : ℝ≥0∞), mul_assoc]
  gcongr
  exact hf x₁ x₂

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