HalaszExceptionalEnergy.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The near-frequency exceptional set can be controlled in mean square without paying for the width of that frequency interval.

lemma OAI.TwoPointCorrelations.halasz_dyadic_sub line 14
lemma OAI.TwoPointCorrelations.halasz_exceptional_coefficient_mass line 20

theorem OAI.TwoPointCorrelations.halasz_exceptional_dyadic_energy line 44

Source documentation

The error from excluding atypical integers costs their density, even when the near-frequency interval grows.

theorem halasz_exceptional_dyadic_energy {ι : Type*} (J : Finset ι)
    (P : ι → Finset ℕ) (F : ℕ → ℂ) (hF : OneBounded F)
    {N : ℕ} (hN : 0 < N) {T : ℝ} (hT : 0 < T) :
    (∫ t in -T..T, ‖mrtDyadicPolynomial F N t -
        mrtDyadicPolynomial (mrtTypicalCoefficient J P F) N t‖ ^ 2) ≤
      8 * Real.exp 1 * (T / N + 2) *
        (((Ioc N (2 * N)).filter (fun n => ¬mrtTypical J P n)).card : ℝ) / N := by
…

Mentions: OAI.TwoPointCorrelations.OneBounded, OAI.TwoPointCorrelations.mrtDyadicPolynomial, OAI.TwoPointCorrelations.mrtTypicalCoefficient, OAI.TwoPointCorrelations.mrtTypical