OrderedCutMatrices.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Ordered matrices at free-word cuts

Subset cut matrices are lifted along the map forgetting the order of a tuple. The exact factorial fibre sizes give the required square-root factorial costs. Complementary-subset adjacency is contractive.

def OAI.KadisonKastler.orderedPreservationMatrix line 29

Source documentation

The preservation matrix with ordered row and column labels.

def orderedPreservationMatrix (W : Finset α) {p q : ℕ}
    (hW : W.card = p + q + 1) (e : α → H →L[ℂ] H) (P : H →L[ℂ] H) (d : ℝ) :
    CStarMatrix (OrderedLabelTuple W q) (OrderedLabelTuple W p) (H →L[ℂ] H) :=
…

Mentions: OAI.KadisonKastler.OrderedLabelTuple

theorem OAI.KadisonKastler.norm_orderedPreservationMatrix_le line 36

Source documentation

Replication costs the square roots of the exact ordering multiplicities.

theorem norm_orderedPreservationMatrix_le (W : Finset α) {p q : ℕ}
    (hW : W.card = p + q + 1) (e : α → H →L[ℂ] H)
    (he : ∀ a, IsStarProjection (e a)) (horth : ∀ a b, a ≠ b → e a * e b = 0)
    (P : H →L[ℂ] H) (hP : IsStarProjection P) {d : ℝ} (hd : 0 < d) :
    ‖orderedPreservationMatrix W hW e P d‖ ≤
      Real.sqrt (p.factorial : ℝ) * Real.sqrt (q.factorial : ℝ) *
        (1 + Real.sqrt (((p + 1 : ℕ) : ℝ) * ((q + 1 : ℕ) : ℝ)) / d) := by
…

Mentions: OAI.KadisonKastler.orderedPreservationMatrix

theorem OAI.KadisonKastler.card_complementary_wordSubsets line 61
Source documentation
A subset of size q has exactly one disjoint complementary subset of size p when the ambient label set has size p + q.
```
theorem card_complementary_wordSubsets (W : Finset α) (p q : ℕ)
    (hW : W.card = p + q) (A : WordSubset W q) :
    #{B : WordSubset W p | Disjoint A.val B.val} = 1 := by
…
```
Mentions: OAI.KadisonKastler.WordSubset
def OAI.KadisonKastler.noPreservationSubsetMatrix line 69
Source documentation
The subset adjacency occurring at a cut with no preservation letter.
```
def noPreservationSubsetMatrix (W : Finset α) (p q : ℕ) :
    CStarMatrix (WordSubset W q) (WordSubset W p) (H →L[ℂ] H) :=
…
```
Mentions: OAI.KadisonKastler.WordSubset
theorem OAI.KadisonKastler.norm_noPreservationSubsetMatrix_le line 73
def OAI.KadisonKastler.orderedNoPreservationMatrix line 94
theorem OAI.KadisonKastler.orderedNoPreservationMatrix_apply line 101
theorem OAI.KadisonKastler.norm_orderedNoPreservationMatrix_le line 106
theorem OAI.KadisonKastler.sqrt_factorial_mul_sqrt_factorial_le line 126
Source documentation
Combining the square-root ordering costs never exceeds the square root of the factorial of the total number of labels.
```
theorem sqrt_factorial_mul_sqrt_factorial_le (p q : ℕ) :
    Real.sqrt (p.factorial : ℝ) * Real.sqrt (q.factorial : ℝ) ≤
      Real.sqrt ((p + q).factorial : ℝ) := by
…
```
theorem OAI.KadisonKastler.norm_orderedNoPreservationMatrix_le_sqrt_factorial line 134
theorem OAI.KadisonKastler.preservation_scalar_sqrt_le line 140

theorem OAI.KadisonKastler.norm_orderedPreservationMatrix_le_sqrt_factorial line 151

Source documentation

The coarser form used when summing preservation cuts of the same word.

theorem norm_orderedPreservationMatrix_le_sqrt_factorial (W : Finset α) {p q : ℕ}
    (hW : W.card = p + q + 1) (e : α → H →L[ℂ] H)
    (he : ∀ a, IsStarProjection (e a)) (horth : ∀ a b, a ≠ b → e a * e b = 0)
    (P : H →L[ℂ] H) (hP : IsStarProjection P) {d : ℝ} (hd : 0 < d) :
    ‖orderedPreservationMatrix W hW e P d‖ ≤
      Real.sqrt ((p + q).factorial : ℝ) * (1 + (p + q + 1 : ℝ) / d) := by
…

Mentions: OAI.KadisonKastler.orderedPreservationMatrix