holder_add_left — Mathlib

English

Holder is additive in the E-component on the left: holder(r,B,f1+f2,g) = holder(r,B,f1,g) + holder(r,B,f2,g).

Русский

Карта Холдер слева по первому аргументу сложения: holder(r,B,f1+f2,g) = holder(r,B,f1,g) + holder(r,B,f2,g).

LaTeX

$$$\\mathrm{holder}(r,B,f_1+f_2,g) = \\mathrm{holder}(r,B,f_1,g) + \\mathrm{holder}(r,B,f_2,g).$$$

Lean4

theorem holder_add_left (f₁ f₂ : Lp E p μ) (g : Lp F q μ) :
    B.holder r (f₁ + f₂) g = B.holder r f₁ g + B.holder r f₂ g :=
  by
  simp only [holder, ← MemLp.toLp_add]
  apply MemLp.toLp_congr
  filter_upwards [AEEqFun.coeFn_add f₁.val f₂.val] with x hx
  simp [hx]

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