opNorm_comp_linearIsometryEquiv — Mathlib

English

nnnorm of identity equals 1 (again).

Русский

nnnorm тождественного отображения снова равна 1.

LaTeX

$$$\\|\\mathrm{id}\\|_{nn} = 1$.$$

Lean4

/-- Precomposition with a linear isometry preserves the operator norm. -/
theorem opNorm_comp_linearIsometryEquiv (f : F →SL[σ₂₃] G) (g : F' ≃ₛₗᵢ[σ₂'] F) :
    ‖f.comp g.toLinearIsometry.toContinuousLinearMap‖ = ‖f‖ :=
  by
  cases subsingleton_or_nontrivial F'
  · haveI := g.symm.toLinearEquiv.toEquiv.subsingleton
    simp
  refine le_antisymm ?_ ?_
  · convert f.opNorm_comp_le g.toLinearIsometry.toContinuousLinearMap
    simp [g.toLinearIsometry.norm_toContinuousLinearMap]
  · convert
      (f.comp g.toLinearIsometry.toContinuousLinearMap).opNorm_comp_le g.symm.toLinearIsometry.toContinuousLinearMap
    · ext
      simp
    haveI := g.symm.surjective.nontrivial
    simp [g.symm.toLinearIsometry.norm_toContinuousLinearMap]

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