unitization_norm_def — Mathlib

English

For x in WithLp 1 (Unitization 𝕜 A), the norm equals the sum of the norms of its first and second coordinates after applying ofLp.

Русский

Для x в WithLp 1 (Unitization 𝕜 A) норма равна сумме норм его первой и второй координат после применения ofLp.

LaTeX

$$$$\\|x\\| = \\|\\mathrm{ofLp} x\\,\\text{.fst}\\| + \\|\\mathrm{ofLp} x\\,\\text{.snd}\\|.$$$$

Lean4

theorem unitization_norm_def (x : WithLp 1 (Unitization 𝕜 A)) : ‖x‖ = ‖(ofLp x).fst‖ + ‖(ofLp x).snd‖ :=
  calc
    ‖x‖ = (‖(ofLp x).fst‖ ^ (1 : ℝ≥0∞).toReal + ‖(ofLp x).snd‖ ^ (1 : ℝ≥0∞).toReal) ^ (1 / (1 : ℝ≥0∞).toReal) :=
      prod_norm_eq_add (by simp : 0 < (1 : ℝ≥0∞).toReal) _
    _ = ‖(ofLp x).fst‖ + ‖(ofLp x).snd‖ := by simp

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