DicksonRow.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Derivation of the norm-two row estimate from the exact little Grothendieck specialization in Haagerup (1983), Theorem 3.2, as quoted in Dickson (2014), Lemmas 2.8–2.9, equations (18)–(22).

def OAI.KadisonSimilarity.LittleGrothendieckInput line 20
Source documentation
Subnormalized states also cover the zero algebra. Only their values on positive squares and their mass bound are used in the application.
```
def LittleGrothendieckInput (A H : Type*) [CStarAlgebra A] [PartialOrder A]
    [StarOrderedRing A] [NormedAddCommGroup H] [InnerProductSpace ℂ H] : Prop :=
…
```
def OAI.KadisonSimilarity.sharpVectorMap line 26
theorem OAI.KadisonSimilarity.sharpVectorMap_apply line 31
theorem OAI.KadisonSimilarity.norm_sharpVectorMap_le line 35

theorem OAI.KadisonSimilarity.dickson_vector_states line 48

Source documentation

The polar estimate converts the two-sided square bound into the single row square, with precisely Dickson's norm-two constant.

theorem dickson_vector_states (lg : LittleGrothendieckInput A H)
    (π : BoundedUnitalHom A H) (hπ : ∀ a, ‖π.1 a‖ ≤ 2 * ‖a‖) (ξ : H) :
    ∃ f g : A →ₚ[ℂ] ℂ, (f 1).re ≤ 1 ∧ (g 1).re ≤ 1 ∧
      ∀ a, ‖(π.1 a).adjoint ξ‖ ^ 2 ≤
        16 * ‖ξ‖ ^ 2 * ((f (a * star a)).re + (g (a * star a)).re) := by
…

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

theorem OAI.KadisonSimilarity.dickson_row_adjoint_sum line 77

Source documentation

The summed adjoint-vector bound for one row.

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

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

theorem OAI.KadisonSimilarity.dickson_rowBound_of_littleGrothendieck line 97
Source documentation
The exact row bound, conditional only on the little Grothendieck input.
```
theorem dickson_rowBound_of_littleGrothendieck (lg : LittleGrothendieckInput A H)
    (π : BoundedUnitalHom A H) (hπ : ∀ a, ‖π.1 a‖ ≤ 2 * ‖a‖) :
    RowBound π.1 (4 * Real.sqrt 2) := by
…
```
Mentions: OAI.KadisonSimilarity.LittleGrothendieckInput, OAI.KadisonSimilarity.BoundedUnitalHom, OAI.KadisonSimilarity.RowBound
theorem OAI.KadisonSimilarity.dicksonTwoBound_of_littleGrothendieck line 131
Source documentation
Both halves of the published norm-two estimate follow from the same little Grothendieck specialization.
```
theorem dicksonTwoBound_of_littleGrothendieck (lg : LittleGrothendieckInput A H) :
    DicksonTwoBound (A := A) H :=
…
```
Mentions: OAI.KadisonSimilarity.LittleGrothendieckInput, OAI.KadisonSimilarity.DicksonTwoBound