norm_extendTo𝕜'_bound — Mathlib

English

The norm of the real number embedded into K equals its real norm.

Русский

Норма вещественного числа, встроенного в K, равна его действительной норме.

LaTeX

$$$\\|\\|z\\|\\|_{\\mathbb{K}} = \\|z\\|$$$

Lean4

/-- The norm of the extension is bounded by `‖fr‖`. -/
theorem norm_extendTo𝕜'_bound (fr : StrongDual ℝ F) (x : F) : ‖(fr.extendTo𝕜' x : 𝕜)‖ ≤ ‖fr‖ * ‖x‖ :=
  by
  set lm : F →L[𝕜] 𝕜 := fr.extendTo𝕜'
  by_cases h : lm x = 0
  · rw [h, norm_zero]
    positivity
  rw [← mul_le_mul_iff_right₀ (norm_pos_iff.2 h), ← sq]
  calc
    ‖lm x‖ ^ 2 = fr (conj (lm x : 𝕜) • x) := fr.toLinearMap.norm_extendTo𝕜'_apply_sq x
    _ ≤ ‖fr (conj (lm x : 𝕜) • x)‖ := (le_abs_self _)
    _ ≤ ‖fr‖ * ‖conj (lm x : 𝕜) • x‖ := (le_opNorm _ _)
    _ = ‖(lm x : 𝕜)‖ * (‖fr‖ * ‖x‖) := by rw [norm_smul, norm_conj, mul_left_comm]

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