BoundedHomRow.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Row bounds for arbitrary bounded homomorphisms in terms of their operator norms.

theorem OAI.KadisonSimilarity.norm_sharpVectorMap_le_general line 17

theorem OAI.KadisonSimilarity.boundedHom_vector_states line 30

Source documentation

The polar estimate converts the two-sided square bound into the single row square, with a bound depending only on the norm of the homomorphism.

theorem boundedHom_vector_states (lg : LittleGrothendieckInput A H)
    (π : BoundedUnitalHom A H) {M : ℝ} (hM : 0 ≤ M) (hπ : ∀ a, ‖π.1 a‖ ≤ M * ‖a‖) (ξ : H) :
    ∃ f g : A →ₚ[ℂ] ℂ, (f 1).re ≤ 1 ∧ (g 1).re ≤ 1 ∧
      ∀ a, ‖(π.1 a).adjoint ξ‖ ^ 2 ≤
        M ^ 4 * ‖ξ‖ ^ 2 * ((f (a * star a)).re + (g (a * star a)).re) := by
…

Mentions: OAI.KadisonSimilarity.LittleGrothendieckInput, OAI.KadisonSimilarity.BoundedUnitalHom

theorem OAI.KadisonSimilarity.boundedHom_row_adjoint_sum line 59

Source documentation

The summed adjoint-vector bound for one row.

theorem boundedHom_row_adjoint_sum (lg : LittleGrothendieckInput A H)
    (π : BoundedUnitalHom A H) {M : ℝ} (hM : 0 ≤ M) (hπ : ∀ a, ‖π.1 a‖ ≤ M * ‖a‖)
    {n : ℕ} (X : Matrix (Fin 1) (Fin n) A) (ξ : H) :
    ∑ j : Fin n, ‖(π.1 (X 0 j)).adjoint ξ‖ ^ 2 ≤
      (2 * M ^ 4) * ‖ξ‖ ^ 2 * ‖CStarMatrix.ofMatrix X‖ ^ 2 := by
…

Mentions: OAI.KadisonSimilarity.LittleGrothendieckInput, OAI.KadisonSimilarity.BoundedUnitalHom

theorem OAI.KadisonSimilarity.boundedHom_rowBound line 79
Source documentation
A row bound uniform over finite rows.
```
theorem boundedHom_rowBound (lg : LittleGrothendieckInput A H)
    (π : BoundedUnitalHom A H) {M : ℝ} (hM : 0 ≤ M) (hπ : ∀ a, ‖π.1 a‖ ≤ M * ‖a‖) :
    RowBound π.1 (2 * M ^ 2) := by
…
```
Mentions: OAI.KadisonSimilarity.LittleGrothendieckInput, OAI.KadisonSimilarity.BoundedUnitalHom, OAI.KadisonSimilarity.RowBound