Model.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

def OAI.AsymptoticallyMinimalLittlewood.littlewoodValue line 8
Source documentation
The Littlewood polynomial of length N, evaluated at z.
Also declared: ComparatorChallenges/AsymptoticallyMinimalLittlewood.lean:7 (same declaration text).
```
def littlewoodValue {N : ℕ} (ε : Fin N → ℝ) (z : ℂ) : ℂ :=
…
```
def OAI.AsymptoticallyMinimalLittlewood.IsRealSigning line 12
Source documentation
Real signs in every consecutive degree 0,...,N-1.
Also declared: ComparatorChallenges/AsymptoticallyMinimalLittlewood.lean:10 (same declaration text).
```
def IsRealSigning {N : ℕ} (ε : Fin N → ℝ) : Prop :=
…
```
def OAI.AsymptoticallyMinimalLittlewood.MainStatement line 15
Also declared: ComparatorChallenges/AsymptoticallyMinimalLittlewood.lean:13 (same declaration text).