Bounds.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Fourier vanishing and bounds on mutually unbiased bases, using actual mixed moments and the six-to-seven completion theorem.

theorem OAI.MUB6.no_seven_mutually_unbiased_bases line 17
Source documentation
Endpoint 2: seven mutually unbiased orthonormal bases in ℂ⁶ cannot exist.
```
theorem no_seven_mutually_unbiased_bases : ¬Attainable 7 := by
…
```
Mentions: OAI.MUB6.Attainable
theorem OAI.MUB6.six_extend_to_seven line 28
Source documentation
Weiner completion in dimension six, preserving all six original bases.
```
theorem six_extend_to_seven : SixExtendToSeven :=
…
```
Mentions: OAI.MUB6.SixExtendToSeven
theorem OAI.MUB6.family_size_le_five line 32
Source documentation
Every finite family of mutually unbiased bases in ℂ⁶ has size at most five.
```
theorem family_size_le_five (n : ℕ) (hn : Attainable n) : n ≤ 5 :=
…
```
Mentions: OAI.MUB6.Attainable
theorem OAI.MUB6.N6_le_five line 37
Source documentation
Endpoint 3, with N6 defined as the supremum of attainable family sizes.
```
theorem N6_le_five : N6 ≤ 5 :=
…
```
Mentions: OAI.MUB6.N6