OAI/Analysis/KadisonKastler/DensePairingBound.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonKastler.opNorm_le_of_dense_pairing line 16

   Source documentation

   A homogeneous pairing estimate on a dense image controls the operator norm. This is used after the finite randomization and clipping argument.

   theorem opNorm_le_of_dense_pairing (J : A → H) (hJ : DenseRange J)
       (V : H →L[ℂ] H) {C : ℝ} (hC : 0 ≤ C)
       (hbound : ∀ a b, ‖inner ℂ (V (J a)) (J b)‖ ≤ C * ‖J a‖ * ‖J b‖) :
       ‖V‖ ≤ C := by
   …

2. theorem OAI.KadisonKastler.opNorm_le_of_dense_unit_pairing line 29

   Source documentation

   It suffices to test the unit vectors in a dense linear image.

   theorem opNorm_le_of_dense_unit_pairing (J : A →ₗ[ℂ] H) (hJ : DenseRange J)
       (V : H →L[ℂ] H) {C : ℝ} (hC : 0 ≤ C)
       (hbound : ∀ a b, ‖J a‖ ≤ 1 → ‖J b‖ ≤ 1 → ‖inner ℂ (V (J a)) (J b)‖ ≤ C) :
       ‖V‖ ≤ C := by
   …