FreeCompressionGeometry.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

The overlap of a small corner with words starting in the other free factor. The estimate follows from the displayed tensor geometry.

theorem OAI.KadisonSimilarity.norm_hilbertTensorInsert_le line 18
theorem OAI.KadisonSimilarity.hilbertTensorInsert_adjoint_comp line 25
Source documentation
The unit vector insertion is an isometry, expressed by its adjoint.
```
theorem hilbertTensorInsert_adjoint_comp (Ω : E) (hΩ : ‖Ω‖ = 1) :
    (hilbertTensorInsert (H := F) Ω).adjoint.comp (hilbertTensorInsert Ω) =
…
```
Mentions: OAI.KadisonSimilarity.hilbertTensorInsert
def OAI.KadisonSimilarity.firstLetterProjection line 39
Source documentation
Projection onto the chosen first tensor coordinate and a tail subspace.
```
def firstLetterProjection (Ω : E) (Q : F →L[ℂ] F) :
    HilbertTensor E F →L[ℂ] HilbertTensor E F :=
…
```
Mentions: OAI.KadisonSimilarity.HilbertTensor
theorem OAI.KadisonSimilarity.firstLetterProjection_idempotent line 43
theorem OAI.KadisonSimilarity.firstLetterProjection_adjoint line 58
theorem OAI.KadisonSimilarity.norm_corner_firstLetterProjection_le line 66
Source documentation
Multiplication in the first factor only sees the small vector eΩ on the range of the first-letter projection.
```
theorem norm_corner_firstLetterProjection_le
    (Ω eΩ : E) (hΩ : ‖Ω‖ = 1) (Q : F →L[ℂ] F) (hQ : ‖Q‖ ≤ 1)
    (e : HilbertTensor E F →L[ℂ] HilbertTensor E F)
    (hact : ∀ x : F, e (hilbertTensorInsert Ω x) = hilbertTensorInsert eΩ x) :
    ‖e * firstLetterProjection Ω Q‖ ≤ ‖eΩ‖ := by
…
```
Mentions: OAI.KadisonSimilarity.HilbertTensor, OAI.KadisonSimilarity.hilbertTensorInsert, OAI.KadisonSimilarity.firstLetterProjection

theorem OAI.KadisonSimilarity.norm_corner_overlap_le line 91

Source documentation

The tracial vector identity gives the square-root overlap in both orders.

theorem norm_corner_overlap_le
    (Ω eΩ : E) (hΩ : ‖Ω‖ = 1) (Q : F →L[ℂ] F)
    (hQ : Q.adjoint = Q) (hQnorm : ‖Q‖ ≤ 1)
    (e : HilbertTensor E F →L[ℂ] HilbertTensor E F) (he : e.adjoint = e)
    (hact : ∀ x : F, e (hilbertTensorInsert Ω x) = hilbertTensorInsert eΩ x)
    {u : ℝ} (hu : 0 ≤ u) (hsq : ‖eΩ‖ ^ 2 = u) :
    ‖e * firstLetterProjection Ω Q‖ ≤ Real.sqrt u ∧
      ‖firstLetterProjection Ω Q * e‖ ≤ Real.sqrt u := by
…

Mentions: OAI.KadisonSimilarity.HilbertTensor, OAI.KadisonSimilarity.hilbertTensorInsert, OAI.KadisonSimilarity.firstLetterProjection

theorem OAI.KadisonSimilarity.norm_free_compression_from_tensor_geometry line 112

Source documentation

The free-letter three blocks and the first-coordinate geometry give the full norm bound for a compressed centered selfadjoint letter.

theorem norm_free_compression_from_tensor_geometry
    (Ω eΩ : E) (hΩ : ‖Ω‖ = 1) (Q : F →L[ℂ] F)
    (hQ : Q.adjoint = Q) (hQsq : Q * Q = Q) (hQnorm : ‖Q‖ ≤ 1)
    (e T : HilbertTensor E F →L[ℂ] HilbertTensor E F)
    (he : e.adjoint = e) (hesq : e * e = e)
    (hact : ∀ x : F, e (hilbertTensorInsert Ω x) = hilbertTensorInsert eΩ x)
    {u b₂ : ℝ} (hu : 0 ≤ u) (hsq : ‖eΩ‖ ^ 2 = u) (hb₂ : 0 ≤ b₂)
    (hzero : (1 - firstLetterProjection Ω Q) * T * (1 - firstLetterProjection Ω Q) = 0)
    (hcreate : ‖firstLetterProjection Ω Q * T * (1 - firstLetterProjection Ω Q)‖ ≤ b₂)
    (hannihilate : ‖(1 - firstLetterProjection Ω Q) * T * firstLetterProjection Ω Q‖ ≤ b₂) :
    ‖e * T * e‖ ≤ 2 * Real.sqrt u * b₂ + u * ‖T‖ := by
…

Mentions: OAI.KadisonSimilarity.HilbertTensor, OAI.KadisonSimilarity.hilbertTensorInsert, OAI.KadisonSimilarity.firstLetterProjection

theorem OAI.KadisonSimilarity.norm_annihilation_eq_creation line 131
Source documentation
For a selfadjoint free letter the annihilation block is adjoint to the creation block, so only the latter needs to be estimated.
```
theorem norm_annihilation_eq_creation
    (P T : HilbertTensor E F →L[ℂ] HilbertTensor E F)
    (hP : P.adjoint = P) (hT : T.adjoint = T) :
    ‖(1 - P) * T * P‖ = ‖P * T * (1 - P)‖ := by
…
```
Mentions: OAI.KadisonSimilarity.HilbertTensor

theorem OAI.KadisonSimilarity.norm_narrow_arc_from_tensor_geometry line 145

Source documentation

The narrow arc has an order-u compression solely from the tensor geometry, the standard creation block, and its scalar moment bounds.

theorem norm_narrow_arc_from_tensor_geometry
    (Ω eΩ : E) (hΩ : ‖Ω‖ = 1) (Q : F →L[ℂ] F)
    (hQ : Q.adjoint = Q) (hQsq : Q * Q = Q) (hQnorm : ‖Q‖ ≤ 1)
    (e T : HilbertTensor E F →L[ℂ] HilbertTensor E F)
    (he : e.adjoint = e) (hesq : e * e = e) (hT : T.adjoint = T)
    (hact : ∀ x : F, e (hilbertTensorInsert Ω x) = hilbertTensorInsert eΩ x)
    {u b₂ : ℝ} (hu : 0 ≤ u) (hsq : ‖eΩ‖ ^ 2 = u) (hb₂ : 0 ≤ b₂)
    (hzero : (1 - firstLetterProjection Ω Q) * T * (1 - firstLetterProjection Ω Q) = 0)
    (hcreate : ‖firstLetterProjection Ω Q * T * (1 - firstLetterProjection Ω Q)‖ ≤ b₂)
    (h₂ : b₂ ^ 2 ≤ u) (hnorm : ‖T‖ ≤ 1) :
    ‖e * T * e‖ ≤ 3 * u := by
…

Mentions: OAI.KadisonSimilarity.HilbertTensor, OAI.KadisonSimilarity.hilbertTensorInsert, OAI.KadisonSimilarity.firstLetterProjection