FlatnessModel.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

def OAI.AsymptoticallyMinimalLittlewoodFiniteFlatness.littlewoodValue line 12
Source documentation
The consecutive-degree polynomial of a real coefficient family.
Also declared: ComparatorChallenges/LittlewoodFiniteFlatness.lean:12 (same declaration text).
```
def littlewoodValue {N : ℕ} (ε : Fin N → ℝ) (z : ℂ) : ℂ :=
…
```
def OAI.AsymptoticallyMinimalLittlewoodFiniteFlatness.IsRealSigning line 16
Source documentation
Every coefficient is a real sign.
Also declared: ComparatorChallenges/LittlewoodFiniteFlatness.lean:16 (same declaration text).
```
def IsRealSigning {N : ℕ} (ε : Fin N → ℝ) : Prop :=
…
```
def OAI.AsymptoticallyMinimalLittlewoodFiniteFlatness.MainStatement line 19
Also declared: ComparatorChallenges/LittlewoodFiniteFlatness.lean:19 (same declaration text).