TierParameters.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Quantitative radius parameter used by the chronological tiers in §07. Constants are explicit and independent of the metric and the horizon.

def OAI.UniformKServer.TierParameters.cutoff line 13
theorem OAI.UniformKServer.TierParameters.cutoff_two line 15
theorem OAI.UniformKServer.TierParameters.radius_parameter line 24
Source documentation
The cutoff can be exponentially large in the tier, but the radius slope is linear in that tier. No dependence on the number of records is introduced.
```
theorem radius_parameter (C h : ℝ) (hC : 1 ≤ C) (hh : 1 ≤ h) :
    Real.log (1+(cutoff C h:ℝ)^2) ≤ (2*C+4)*h := by
…
```
Mentions: OAI.UniformKServer.TierParameters.cutoff