CountGeometryParameters.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Fixed powers supplying the witness dilation and popularity threshold.

theorem OAI.LipschitzHilbert.count_witness_dilation line 11
theorem OAI.LipschitzHilbert.count_popular_threshold line 29
Source documentation
One extra power of L absorbs the compact-extraction and interval constants in the popularity average.
```
theorem count_popular_threshold {L a p t : ℝ} (hL : 8 ≤ L)
    (ht : 2 * a + p + 1 ≤ t) :
    L ^ (-t) ≤ L ^ (-a) / (8 * L ^ a * L ^ p) := by
…
```