Model.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

def OAI.SubpolynomialLp.coordinateDistance line 12
Also declared: ComparatorChallenges/SubpolynomialLp.lean:12 (same declaration text).
def OAI.SubpolynomialLp.GoodDimension line 16
Source documentation
The universal property used in the definition of d_p(n,D).
Also declared: ComparatorChallenges/SubpolynomialLp.lean:16 (same declaration text).
```
def GoodDimension (p : ℝ) (n : ℕ) (D : ℝ) (d : ℕ) : Prop :=
…
```
def OAI.SubpolynomialLp.dimension line 26
Source documentation
The least universal coordinate dimension. The theorem also asserts that this least dimension has the defining property, ruling out an empty infimum.
Also declared: ComparatorChallenges/SubpolynomialLp.lean:26 (same declaration text).
```
def dimension (p : ℝ) (n : ℕ) (D : ℝ) : ℕ :=
…
```
def OAI.SubpolynomialLp.gamma line 29
Also declared: ComparatorChallenges/SubpolynomialLp.lean:29 (same declaration text).