LocalHeadDiscard.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The original head only requires normality at the largest local cutoff.

lemma OAI.TotientAsymptotic.local_head_normality_decay line 14
theorem OAI.TotientAsymptotic.local_non_normal_head_count line 43
Source documentation
Uniform over subsets of the local grid: the head exclusion is negligible relative to the same prefix volume used by the positive construction.
```
theorem local_non_normal_head_count {c : ℝ} (hc : 0 < c) (d : ℕ) (hd : 0 < d) :
    ∀ L : ℕ,∀ᶠ H : ℕ in atTop,∀ᶠ x : ℝ in atTop,
      ∀ Q : Finset (Fin (m x-H) → ℕ),
      Q ⊆ gridPrimeTuples (localPrimeGrid x c L (m x-H)) →
      ((nonNormalHeadPairs x (localNormalityScale (m x)) d Q).card:ℝ) ≤
        (x/(d*Real.log x))*rho^(m x)*G x (m x-H) := by
…
```
Mentions: OAI.TotientAsymptotic.L, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.gridPrimeTuples, OAI.TotientAsymptotic.localPrimeGrid, OAI.TotientAsymptotic.nonNormalHeadPairs, OAI.TotientAsymptotic.localNormalityScale, OAI.TotientAsymptotic.rho, OAI.TotientAsymptotic.G