OAI/Analysis/KadisonKastler/ScalarNormMinimizer.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A nearest scalar operator in the ambient norm

  1. theorem OAI.KadisonKastler.exists_scalar_norm_minimizer line 16

    Source documentation

    Compactness of a scalar disk gives a nearest scalar operator.

    theorem exists_scalar_norm_minimizer (a : H →L[ℂ] H) :
    ∃ z : ℂ, ∀ w : ℂ, ‖a - z • (1 : H →L[ℂ] H)‖ ≤ ‖a - w • 1‖ := by
…