HalaszPrimePowers.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The total reciprocal contribution of higher prime powers is finite. The convergence theorem is already in Mathlib; only its modulus-one specialization and the finite hyperbola error are needed here.

def OAI.TwoPointCorrelations.halaszPrimePowerWeight line 15
Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszPrimePowers.lean:15 (same declaration text).
lemma OAI.TwoPointCorrelations.halaszPrimePowerWeight_nonneg line 18
Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszPrimePowers.lean:18 (same declaration text).
lemma OAI.TwoPointCorrelations.halaszPrimePowerWeight_summable line 24
Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszPrimePowers.lean:24 (same declaration text).
def OAI.TwoPointCorrelations.halaszPrimePowerConstant line 34
Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszPrimePowers.lean:34 (same declaration text).
lemma OAI.TwoPointCorrelations.halaszPrimePowerConstant_nonneg line 37
Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszPrimePowers.lean:37 (same declaration text).
lemma OAI.TwoPointCorrelations.halasz_bounded_prefix_norm line 40
Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszPrimePowers.lean:40 (same declaration text).
theorem OAI.TwoPointCorrelations.halasz_prime_power_error line 50
Source documentation
Discarding all higher prime powers in the logarithmic hyperbola incurs at most an absolute constant times its outer cutoff.
Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszPrimePowers.lean:50 (same declaration text).
```
theorem halasz_prime_power_error (f : ℕ → ℂ) (hf : OneBounded f) (N : ℕ) :
    ‖∑ d ∈ Icc 1 N, (halaszPrimePowerWeight d : ℂ) * f d *
      (∑ m ∈ Icc 1 (N / d), f m)‖ ≤ (N : ℝ) * halaszPrimePowerConstant := by
…
```
Mentions: OAI.TwoPointCorrelations.OneBounded, OAI.TwoPointCorrelations.halaszPrimePowerWeight, OAI.TwoPointCorrelations.halaszPrimePowerConstant