HalaszUnitRenormalization.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Elementary near-twist renormalization using the absolute unit correction. The power-sum error is uniform in the summation cutoff and linear in the twist.

def OAI.TwoPointCorrelations.halaszPhaseMean line 13
Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszUnitRenormalization.lean:13 (same declaration text).
def OAI.TwoPointCorrelations.halaszUnitMain line 16
Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszUnitRenormalization.lean:16 (same declaration text).
lemma OAI.TwoPointCorrelations.halasz_power_phase_mul line 19
Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszUnitRenormalization.lean:19 (same declaration text).
lemma OAI.TwoPointCorrelations.halasz_phase_factor_norm line 24
Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszUnitRenormalization.lean:24 (same declaration text).
lemma OAI.TwoPointCorrelations.halasz_phase_mean_hyperbola line 31
Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszUnitRenormalization.lean:31 (same declaration text).
lemma OAI.TwoPointCorrelations.halasz_phase_main_local line 64
Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszUnitRenormalization.lean:64 (same declaration text).
theorem OAI.TwoPointCorrelations.halasz_phase_mean_main_error line 79
Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszUnitRenormalization.lean:79 (same declaration text).
theorem OAI.TwoPointCorrelations.halasz_unit_renormalization line 118
Source documentation
A cutoff-uniform renormalization. Only the absolute correction mass is needed; its near-center saving is supplied by halasz_near_correction_mean.
Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszUnitRenormalization.lean:118 (same declaration text).
```
theorem halasz_unit_renormalization (F : ℕ → ℂ) (hF : Multiplicative F)
    (hF1 : F 1 = 1) (t : ℝ) (N : ℕ) :
    ‖halaszPhaseMean F t N -
      (halaszPowerPhase t N / (1 + (-t : ℂ) * Complex.I)) * halaszPhaseMean F 0 N‖ ≤
      18 * (1 + |t|) * ∑ d ∈ Icc 1 N, ‖halaszUnitCorrection F d‖ := by
…
```
Mentions: OAI.TwoPointCorrelations.Multiplicative, OAI.TwoPointCorrelations.halaszPhaseMean, OAI.TwoPointCorrelations.halaszPowerPhase, OAI.TwoPointCorrelations.halaszUnitCorrection