norm_extendTo𝕜'_apply_sq — Mathlib

English

The squared norm of the extended functional at x equals fr(conj(fr'(x)) x).

Русский

Квадрат нормы расширенного функционала в x равен fr(conj(fr'(x)) x).

LaTeX

$$$ \\|\\big(fr.extendTo𝕜'(x)\\big)\\|^{2} = fr\\Big(\\overline{fr\\big( (1) \\cdot x \\big)} \\cdot x\\Big)$$$

Lean4

theorem norm_extendTo𝕜'_apply_sq (fr : Dual ℝ F) (x : F) :
    ‖(fr.extendTo𝕜' x : 𝕜)‖ ^ 2 = fr (conj (fr.extendTo𝕜' x : 𝕜) • x) :=
  calc
    ‖(fr.extendTo𝕜' x : 𝕜)‖ ^ 2 = re (conj (fr.extendTo𝕜' x) * fr.extendTo𝕜' x : 𝕜) := by
      rw [RCLike.conj_mul, ← ofReal_pow, ofReal_re]
    _ = fr (conj (fr.extendTo𝕜' x : 𝕜) • x) := by rw [← smul_eq_mul, ← map_smul, extendTo𝕜'_apply_re]

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