English
The extended Holder norm satisfies subadditivity: eHolderNorm r (f + g) ≤ eHolderNorm r f + eHolderNorm r g.
Русский
Расширенная норма Холдера удовлетворяет неравенству по сумме: eHolderNorm r (f + g) ≤ eHolderNorm r f + eHolderNorm r g.
LaTeX
$$$eHolderNorm\, r\; (f + g) \le eHolderNorm\, r\; f + eHolderNorm\, r\; g$$$
Lean4
theorem eHolderNorm_add_le : eHolderNorm r (f + g) ≤ eHolderNorm r f + eHolderNorm r g :=
by
by_cases hfg : MemHolder r f ∧ MemHolder r g
· obtain ⟨hf, hg⟩ := hfg
rw [← hf.coe_nnHolderNorm_eq_eHolderNorm, ← hg.coe_nnHolderNorm_eq_eHolderNorm, ←
(hf.add hg).coe_nnHolderNorm_eq_eHolderNorm, ← coe_add, ENNReal.coe_le_coe]
exact hf.nnHolderNorm_add_le hg
· rw [Classical.not_and_iff_not_or_not, ← eHolderNorm_eq_top, ← eHolderNorm_eq_top] at hfg
obtain (h | h) := hfg
all_goals simp [h]
