holder_smul_right — Mathlib

English

Scaling the F-component on the right by a scalar c commutes with the Holder map on the right: B.holder(r,f,g) = B.holder(r,f,c•g) = c•B.holder(r,f,g).

Русский

Умножение второй компоненты на скаляр слева сохраняется в Holder-map: holder(r,f,c•g) = c•holder(r,f,g).

LaTeX

$$$\\mathrm{holder}(r,B,f, c\\cdot g) = c\\cdot \\mathrm{holder}(r,B,f,g).$$$

Lean4

theorem holder_smul_right (c : 𝕜) (f : Lp E p μ) (g : Lp F q μ) : B.holder r f (c • g) = c • B.holder r f g :=
  by
  simp only [holder, ← MemLp.toLp_const_smul]
  apply MemLp.toLp_congr
  filter_upwards [Lp.coeFn_smul c g] with x hx
  simp [hx]

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