HalaszConstantGrowth.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Polynomial-in-the-degree control of the logarithm of the explicit iteration constant. The absolute prime-supply threshold is retained.

lemma OAI.TwoPointCorrelations.four_terms line 9
lemma OAI.TwoPointCorrelations.halasz_iteration_threshold_growth line 16
lemma OAI.TwoPointCorrelations.halasz_iteration_base_growth line 51
theorem OAI.TwoPointCorrelations.halasz_selected_constant_growth line 100
Source documentation
The constant at the selected moment has logarithm O(k^4 log k). No endpoint-dependent constant is hidden.
```
theorem halasz_selected_constant_growth {R₀ k : ℕ} (hk : 2≤k) :
    halaszIterationConstant R₀ k (10*k)≤(R₀+k+32)^(256*k^4) := by
…
```
Mentions: OAI.TwoPointCorrelations.halaszIterationConstant