Orthogonality.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.MUB6.weighted_contraction line 11

Source documentation

The finite orthogonality contraction underlying equation (same-matrix).

theorem weighted_contraction {H : CMatrix} (hH : IsHadamard H)
    (u v : Coord → ℂ) (i : Coord) :
    (∑ j, (∑ k, u k * H i k * conj (H j k)) *
      (∑ l, v l * conj (H i l) * H j l)) =
      6 * ∑ k, u k * v k := by
…

Mentions: OAI.MUB6.CMatrix, OAI.MUB6.IsHadamard, OAI.MUB6.Coord

theorem OAI.MUB6.g_add_difference line 45
theorem OAI.MUB6.same_matrix_identity line 58
Source documentation
Source Lemma (basic), equation (same-matrix), for arbitrary integral charges.
```
theorem same_matrix_identity {H : CMatrix} (hH : IsHadamard H)
    (a b : Charge) (i : Coord) :
    ∑ j, g H (a + difference i j) * g H (b + difference j i) = g H (a + b) := by
…
```
Mentions: OAI.MUB6.CMatrix, OAI.MUB6.IsHadamard, OAI.MUB6.Charge, OAI.MUB6.Coord, OAI.MUB6.g, OAI.MUB6.difference