holder_add_right — Mathlib

English

Holder is additive in the F-component on the right: holder(r,f,g1+g2) = holder(r,f,g1) + holder(r,f,g2).

Русский

Holder слева по второму аргументу сложение: holder(r,f,g1+g2) = holder(r,f,g1) + holder(r,f,g2).

LaTeX

$$$\\mathrm{holder}(r,B,f,g_1+g_2) = \\mathrm{holder}(r,B,f,g_1) + \\mathrm{holder}(r,B,f,g_2).$$$

Lean4

theorem holder_add_right (f : Lp E p μ) (g₁ g₂ : Lp F q μ) :
    B.holder r f (g₁ + 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 g₁.val g₂.val] with x hx
  simp [hx]

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