FockRelations.lean`

21 declarations, 0 contain sorry, 0 declared as axioms

Structural free diagonal data and its consequences

This structure records the projection, support, covariance, and decomposition identities of a free diagonal representation. Norm bounds are consequences, not fields. No existence theorem for the structure is assumed here.

structure OAI.KadisonKastler.FreeDiagonalModel line 28
def OAI.KadisonKastler.FreeDiagonalModel.centered line 51
def OAI.KadisonKastler.FreeDiagonalModel.D line 54
theorem OAI.KadisonKastler.FreeDiagonalModel.centered_eq line 56
theorem OAI.KadisonKastler.FreeDiagonalModel.star_creation_right_support line 60
theorem OAI.KadisonKastler.FreeDiagonalModel.creation_mul_P line 65
theorem OAI.KadisonKastler.FreeDiagonalModel.P_mul_star_creation line 70
theorem OAI.KadisonKastler.FreeDiagonalModel.D_left_support line 74
theorem OAI.KadisonKastler.FreeDiagonalModel.D_right_support line 77
theorem OAI.KadisonKastler.FreeDiagonalModel.mul_eq_zero_of_orthogonal_support line 81
theorem OAI.KadisonKastler.FreeDiagonalModel.star_creation_mul_creation line 90
Source documentation
The four zero products used by the cut expansion follow from orthogonality of the first-copy projections.
```
theorem star_creation_mul_creation {i j : ι} (hij : i ≠ j) (a b : α) :
    star (M.C i a) * M.C j b = 0 :=
…
```
theorem OAI.KadisonKastler.FreeDiagonalModel.star_creation_mul_D line 95
theorem OAI.KadisonKastler.FreeDiagonalModel.D_mul_creation line 100
theorem OAI.KadisonKastler.FreeDiagonalModel.D_mul_D line 105

theorem OAI.KadisonKastler.FreeDiagonalModel.norm_creation_row_le line 110

Source documentation

The covariance identity gives the complete creation-row norm.

theorem norm_creation_row_le (i : ι) :
    ‖(CStarMatrix.ofMatrix (fun (_ : Unit) a => M.C i a))‖ ≤
      (Real.sqrt (Fintype.card α : ℝ))⁻¹ :=
…

theorem OAI.KadisonKastler.FreeDiagonalModel.norm_creation_le line 115
theorem OAI.KadisonKastler.FreeDiagonalModel.norm_star_creation_le line 121

theorem OAI.KadisonKastler.FreeDiagonalModel.norm_projection_sub_smul_one_le line 127

Source documentation

A projection centered by any scalar in [0,1] remains contractive.

private theorem norm_projection_sub_smul_one_le (E : H →L[ℂ] H)
    (hE : IsStarProjection E) {t : ℝ} (ht0 : 0 ≤ t) (ht1 : t ≤ 1) :
    ‖E - (t : ℂ) • (1 : H →L[ℂ] H)‖ ≤ 1 := by
…

theorem OAI.KadisonKastler.FreeDiagonalModel.norm_centered_le line 145
theorem OAI.KadisonKastler.FreeDiagonalModel.norm_D_le line 151

theorem OAI.KadisonKastler.FreeDiagonalModel.norm_centered_word_le line 165

Source documentation

The structural model therefore supplies all analytic and algebraic inputs to the proved single-centered-word estimate.

theorem norm_centered_word_le (label : ι → α) (l : List ι) (hl : l.Nodup) :
    ‖(l.map (fun i => M.centered i (label i))).prod‖ ≤
      (2 * l.length + 1 : ℝ) /
        Real.sqrt ((Fintype.card α : ℝ) ^ (l.length - 1)) := by
…