IncidenceMatrices.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Incidence matrices in the free-word cuts

A matrix supported on a relation with row degree at most R and column degree at most C, and contractive operator entries, has norm at most sqrt (R * C). The scalar correction in a preservation cut has precisely this form.

theorem OAI.KadisonKastler.norm_matrix_le_sqrt_degrees line 31

Source documentation

The row-column degree estimate, with the actual Hilbert-space matrix norm.

theorem norm_matrix_le_sqrt_degrees (T : CStarMatrix I J (H →L[ℂ] H))
    (E : I → J → Prop) [DecidableRel E] (R C : ℕ)
    (hzero : ∀ i j, ¬ E i j → T i j = 0)
    (hentry : ∀ i j, ‖T i j‖ ≤ 1)
    (hrow : ∀ i, #{j | E i j} ≤ R)
    (hcol : ∀ j, #{i | E i j} ≤ C) :
    ‖T‖ ≤ Real.sqrt ((R : ℝ) * C) := by
…

abbrev OAI.KadisonKastler.WordSubset line 93
Source documentation
The subset indices left after grouping the ordered labels of a cut.
```
abbrev WordSubset (W : Finset α) (p : ℕ) := {B : Finset α // B ⊆ W ∧ B.card = p}
```
theorem OAI.KadisonKastler.card_wordSubset line 95
def OAI.KadisonKastler.disjointWordSubsetEquiv line 102
Source documentation
Disjoint columns in one row are precisely the fixed-size subsets of the complement of that row.
```
def disjointWordSubsetEquiv (W : Finset α) (A : Finset α) (p : ℕ) :
    {B : WordSubset W p // Disjoint A B.val} ≃ WordSubset (W \ A) p where
…
```
Mentions: OAI.KadisonKastler.WordSubset
theorem OAI.KadisonKastler.card_disjoint_wordSubsets line 111

theorem OAI.KadisonKastler.norm_preservation_adjacency_le line 121

Source documentation

The scalar adjacency correction in a preservation cut.

theorem norm_preservation_adjacency_le (W : Finset α) (p q : ℕ)
    (hW : W.card = p + q + 1) :
    ‖(CStarMatrix.ofMatrix (fun (A : WordSubset W q) (B : WordSubset W p) =>
      if Disjoint A.val B.val then (1 : H →L[ℂ] H) else 0))‖ ≤
      Real.sqrt (((p + 1 : ℕ) : ℝ) * ((q + 1 : ℕ) : ℝ)) := by
…

Mentions: OAI.KadisonKastler.WordSubset