prod_antilipschitzWith_ofLp — Mathlib

English

There is a LipschitzWith constant (2)^(1/p) for the map toLp p, i.e., Lipschitz bound in the product case.

Русский

Для отображения toLp_p существует константа липшицевости (2)^(1/p) в произведении.

LaTeX

$$$ \\text{LipschitzWith}\\bigl( (2)^{(1/p).toReal} \\bigr)\\bigl( \\operatorname{toLp}_p : (\\alpha \\times \\beta) \\to \\mathrm{WithLp}_p(\\alpha \\times \\beta) \\bigr)$$$

Lean4

theorem prod_antilipschitzWith_ofLp [PseudoEMetricSpace α] [PseudoEMetricSpace β] :
    AntilipschitzWith ((2 : ℝ≥0) ^ (1 / p).toReal) (@ofLp p (α × β)) :=
  prod_antilipschitzWith_ofLp_aux p α β

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