ComplementAlgebra.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Algebra of the missing-basis projection

The six diagonal expectation operators and the trace operator satisfy a small multiplication table. The proof shows that the resulting complement operator is idempotent, using ring algebra rather than numerical approximation.

theorem OAI.MUB6.Weiner.sum_pairwise_projection_square line 22

Source documentation

A finite family of idempotents whose off-diagonal products are one common operator has an explicit square for its sum.

theorem sum_pairwise_projection_square {ι : Type*} [Fintype ι] [DecidableEq ι]
    (D : ι → R) (P : R)
    (h : ∀ i j, D i * D j = if i = j then D i else P) :
    (∑ i, D i) * (∑ i, D i) = (∑ i, D i) +
      ((Fintype.card ι : R) ^ 2 - (Fintype.card ι : R)) * P := by
…

theorem OAI.MUB6.Weiner.complement_idempotent line 37
Source documentation
The multiplication table for six unbiased expectation projections makes 1 + W - S idempotent, where W is the unnormalized trace operator and S is the sum of the six expectations.
```
theorem complement_idempotent (S W : R)
    (hSS : S * S = S + 5 * W)
    (hSW : S * W = 6 * W) (hWS : W * S = 6 * W)
    (hWW : W * W = 6 * W) :
    (1 + W - S) * (1 + W - S) = 1 + W - S := by
…
```
theorem OAI.MUB6.Weiner.complete_complement_idempotent line 47
Source documentation
The analogous complement for seven expectations in dimension six is also idempotent. Together with its zero trace this yields the complete-family moment identity.
```
theorem complete_complement_idempotent (S W : R)
    (hSS : S * S = S + 7 * W)
    (hSW : S * W = 7 * W) (hWS : W * S = 7 * W)
    (hWW : W * W = 6 * W) :
    (1 + W - S) * (1 + W - S) = 1 + W - S := by
…
```