English
Let hf and hg be MemHolder r f and MemHolder r g. Then the Holder norm of the sum is bounded by the sum of Holder norms: nnHolderNorm r (f + g) ≤ nnHolderNorm r f + nnHolderNorm r g.
Русский
Пусть f и g обладают свойством MemHolder r, тогда нормаHolder для их суммы не превышает сумму норм Holder: nnHolderNorm r (f + g) ≤ nnHolderNorm r f + nnHolderNorm r g.
LaTeX
$$$\text{MemHolder } r f \;\to\; \text{MemHolder } r g \;\Rightarrow\; nnHolderNorm\; r\; (f + g) \le nnHolderNorm\; r\; f + nnHolderNorm\; r\; g$$$
Lean4
theorem nnHolderNorm_add_le (hf : MemHolder r f) (hg : MemHolder r g) :
nnHolderNorm r (f + g) ≤ nnHolderNorm r f + nnHolderNorm r g :=
(hf.add hg).holderWith.nnholderNorm_le.trans <| coe_le_coe.2 (hf.holderWith.add hg.holderWith).nnholderNorm_le
