Completion.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Weiner completion in dimension six

The missing orthonormal basis is obtained by simultaneously diagonalizing the commutative fixed space of the complementary Hilbert--Schmidt projection.

lemma OAI.MUB6.Weiner.unbiased_of_complement_fixed line 18
theorem OAI.MUB6.Weiner.exists_unbiased_basis line 40
Source documentation
Every family of six mutually unbiased orthonormal bases of ℂ⁶ has a seventh orthonormal basis unbiased to each of them.
```
theorem exists_unbiased_basis (B : Fin 6 → MUB6.Basis) (hB : IsMUBFamily B) :
    ∃ b : MUB6.Basis, ∀ r i j,
      Complex.normSq (inner ℂ (B r i) (b j)) = (1 : ℝ) / 6 := by
…
```
Mentions: OAI.MUB6.Basis, OAI.MUB6.IsMUBFamily
def OAI.MUB6.Weiner.appendBasis line 56
Source documentation
Append the basis supplied by the completion theorem.
```
noncomputable def appendBasis (B : Fin 6 → MUB6.Basis) (b : MUB6.Basis) :
    Fin 7 → MUB6.Basis := Fin.lastCases b B
```
Mentions: OAI.MUB6.Basis
lemma OAI.MUB6.Weiner.appendBasis_castSucc line 59
lemma OAI.MUB6.Weiner.appendBasis_last line 62
lemma OAI.MUB6.Weiner.appendBasis_isMUB line 66
theorem OAI.MUB6.Weiner.six_extend_to_seven line 89
Source documentation
Weiner's completion theorem, specialized to six-dimensional complex Hilbert space, with the original six bases retained at their original indices.
```
theorem six_extend_to_seven (B : Fin 6 → MUB6.Basis) (hB : IsMUBFamily B) :
    ∃ C : Fin 7 → MUB6.Basis, IsMUBFamily C ∧ ∀ r, C r.castSucc = B r := by
…
```
Mentions: OAI.MUB6.Basis, OAI.MUB6.IsMUBFamily