MomentContraction.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Orthogonality relations for injective moments. The saturated relation uses only six-row moments, even though its generating exponent array has seven rows.

def OAI.MUB6.rowMonomial line 14
def OAI.MUB6.mergeFirst line 17
def OAI.MUB6.contractionMonomial line 21
theorem OAI.MUB6.rowMonomial_difference line 26
theorem OAI.MUB6.rowMonomial_sum_zero line 39
theorem OAI.MUB6.contractionMonomial_sum_zero line 46
theorem OAI.MUB6.contractionMonomial_new line 54
theorem OAI.MUB6.contractionMonomial_occupied line 63
def OAI.MUB6.contractionIntegrand line 73
theorem OAI.MUB6.contractionIntegrand_sum_zero line 79

theorem OAI.MUB6.injectiveMoment_first_row_contraction line 91

Source documentation

The coefficient is 6-p, where p is the number of rows other than the contracted row. Equivalently it is 7 minus the original row count.

theorem injectiveMoment_first_row_contraction {p q : ℕ} (hp : p < 6)
    {H : CMatrix} (hH : IsHadamard H)
    (A : Matrix (Fin (p + 1)) (Fin q) ℤ) (v w : Fin q) (hvw : v ≠ w)
    (hA : A 0 = Pi.single v 1 - Pi.single w 1) :
    ((6 - p : ℕ) : ℝ) * injectiveMoment H A +
      (∑ j, injectiveMoment H (mergeFirst A j)) = 0 := by
…

Mentions: OAI.MUB6.CMatrix, OAI.MUB6.IsHadamard, OAI.MUB6.injectiveMoment, OAI.MUB6.mergeFirst

theorem OAI.MUB6.injectiveMoment_seven_row_boundary line 115
Source documentation
The seven-row boundary equation. All six terms are moments of six-row matrices. There is no term for sampling seven distinct labels from six.
```
theorem injectiveMoment_seven_row_boundary {q : ℕ} {H : CMatrix} (hH : IsHadamard H)
    (A : Matrix (Fin 7) (Fin q) ℤ) (v w : Fin q) (hvw : v ≠ w)
    (hA : A 0 = Pi.single v 1 - Pi.single w 1) :
    (∑ j : Fin 6, injectiveMoment H (mergeFirst A j)) = 0 := by
…
```
Mentions: OAI.MUB6.CMatrix, OAI.MUB6.IsHadamard, OAI.MUB6.injectiveMoment, OAI.MUB6.mergeFirst