UnbandedLower.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform scaled lower coordinates for the unbanded witness regions.

theorem OAI.TotientAsymptotic.tailPrefixRegion_scaled_lower line 16
Source documentation
The first retained tail prime forces every continuous prefix coordinate above a fixed multiple of H rho^(-h). This is the lower bound needed when thickening tail boxes after removing the prefix bands.
```
theorem tailPrefixRegion_scaled_lower (hford : FordRenewalInput) :
    ∃ c : ℝ, 0 < c ∧ ∀ {x s : ℝ} {H : ℕ} {η : TailDatum H},
      0 ≤ s → IsWitness H s η → P H < H → H ≤ m x →
      ∀ {u : Fin (R x H) → ℝ}, u ∈ tailPrefixRegion x H η →
      ∀ i, c*(H-1 : ℕ) ≤ rho^(m x-(i.val+1))*u i := by
…
```
Mentions: OAI.TotientAsymptotic.FordRenewalInput, OAI.TotientAsymptotic.TailDatum, OAI.TotientAsymptotic.IsWitness, OAI.TotientAsymptotic.P, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.tailPrefixRegion, OAI.TotientAsymptotic.rho