HalaszVinogradovFibers.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Fixing all but k variables in the complete system leaves at most k! solutions. This elementary fiber estimate is the initial counting bound before the translation and differencing steps.

lemma OAI.TwoPointCorrelations.halasz_vinogradov_tail_fiber line 13
theorem OAI.TwoPointCorrelations.halasz_vinogradov_general_fiber line 59
theorem OAI.TwoPointCorrelations.halasz_vinogradov_initial_bound line 71
Source documentation
The elementary complete-system bound, valid before mean-value iteration.
```
theorem halasz_vinogradov_initial_bound (k r N : ℕ) :
    halaszVinogradovCount (k+r) k N ≤ N^(k+2*r)*k.factorial := by
…
```
Mentions: OAI.TwoPointCorrelations.halaszVinogradovCount