BasicCube.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Concrete enclosure of every prime box meeting the basic full tuples.

lemma OAI.TotientAsymptotic.simplexBoxError_eq line 13
lemma OAI.TotientAsymptotic.cube_band_lower line 23
theorem OAI.TotientAsymptotic.basic_prime_box_enclosure line 47
Source documentation
The fixed enlargement C = 4 absorbs the unit-box errors once the smallest retained scale is large. All constants are independent of dimension.
```
theorem basic_prime_box_enclosure {x : ℝ} {H : ℕ}
    (hs : 0 ≤ theta x) (hcut : 4 ≤ lam*(P H : ℝ)) (hB : 0 < B x)
    (hscale : (m x : ℝ)/(B x*rho^(m x)) ≤ 2/lam)
    (hL : 0 < L x H) {η : RemainderDatum (L x H)}
    (hη : IsBasicRemainder x H η) {v : Fin (L x H) → ℝ}
    (hdist : ∀ i, |primePrefixCoord η.primes i-v i| ≤ 1) :
    v ∈ enlargedSimplex (L x H) (B x)
      (1+simplexBoxError 4 (m x))
      (fun i => 1+simplexBoxError 4 (m x-(i.val+1))) := by
…
```
Mentions: OAI.TotientAsymptotic.theta, OAI.TotientAsymptotic.lam, OAI.TotientAsymptotic.P, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.rho, OAI.TotientAsymptotic.L, OAI.TotientAsymptotic.RemainderDatum, OAI.TotientAsymptotic.IsBasicRemainder, OAI.TotientAsymptotic.primePrefixCoord, OAI.TotientAsymptotic.enlargedSimplex, OAI.TotientAsymptotic.simplexBoxError