LocalNormalityDecay.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Indexed normality: a polynomial logarithmic cutoff beats each bounded local tail.

def OAI.TotientAsymptotic.localNormalityScale line 11
lemma OAI.TotientAsymptotic.localNormalityScale_factor line 13
theorem OAI.TotientAsymptotic.local_normality_geometric_decay line 21
Source documentation
The two index choices and every local tuple coordinate are included in this bound. The cutoff U may grow exponentially with the tail length.
```
theorem local_normality_geometric_decay {C D A : ℝ}
    (hC : 0 < C) (hD : 0 < D) (hA : 0 ≤ A) :
    ∀ᶠ h : ℕ in atTop,∀ U : ℝ,1 ≤ U → Real.log (6*U) ≤ A*h →
      ∀ n : ℕ,n ≤ h →
        (h:ℝ)^2*(C*(2*U+2)^6*Real.exp (-(h:ℝ)^4/6))*(D*(2*U+2))^n ≤ rho^h := by
…
```
Mentions: OAI.TotientAsymptotic.D, OAI.TotientAsymptotic.A, OAI.TotientAsymptotic.rho