instProdIsBoundedSMul — Mathlib

English

Assuming a scalar field 𝕜 with appropriate structure, the action of 𝕜 on WithLp p (α × β) is bounded; i.e., scalar multiplication is controlled compatibly with the Lp-norm.

Русский

При условии наличия подходящей структуры скалярного умножения, действие скаляра 𝕜 на WithLp p (α × β) ограничено; скалярное умножение контролируется нормой Lp.

LaTeX

$$$\text{IsBoundedSMul }\, 𝕜\; (WithLp\ p\ (α \times β)).$$$

Lean4

instance instProdIsBoundedSMul : IsBoundedSMul 𝕜 (WithLp p (α × β)) :=
  .of_nnnorm_smul_le fun c f => by
    rcases p.dichotomy with (rfl | hp)
    · simp only [← prod_nnnorm_ofLp, ofLp_smul]
      exact norm_smul_le _ _
    · have hp0 : 0 < p.toReal := zero_lt_one.trans_le hp
      have hpt : p ≠ ⊤ := p.toReal_pos_iff_ne_top.mp hp0
      rw [prod_nnnorm_eq_add hpt, prod_nnnorm_eq_add hpt, one_div, NNReal.rpow_inv_le_iff hp0, NNReal.mul_rpow, ←
        NNReal.rpow_mul, inv_mul_cancel₀ hp0.ne', NNReal.rpow_one, mul_add, ← NNReal.mul_rpow, ← NNReal.mul_rpow]
      exact
        add_le_add (NNReal.rpow_le_rpow (nnnorm_smul_le _ _) hp0.le) (NNReal.rpow_le_rpow (nnnorm_smul_le _ _) hp0.le)

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