HalaszNearEnergy.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Conversion of the centered prefix comparison into the actual dyadic Fourier energy. The main term is integrated with its exact Cauchy kernel.

lemma OAI.TwoPointCorrelations.halasz_dyadic_phase line 14
lemma OAI.TwoPointCorrelations.halasz_phase_factor_sq line 29
lemma OAI.TwoPointCorrelations.halasz_near_dyadic_bound line 35
lemma OAI.TwoPointCorrelations.halasz_near_dyadic_square line 62

theorem OAI.TwoPointCorrelations.halasz_near_dyadic_energy line 82

Source documentation

Only the squared renormalization error pays for the length of the near-center frequency interval.

theorem halasz_near_dyadic_energy (F : ℕ → ℂ) {N : ℕ} (hN : 0 < N)
    (A E U : ℝ) (hA : 0 ≤ A) (hE : 0 ≤ E) (hU : 0 ≤ U)
    (hcenter : ∀ k ∈ Icc N (2 * N), ‖halaszPhaseMean F 0 k‖ ≤ A * k)
    (hnear : ∀ u ∈ Set.Icc (-U) U, ∀ k ∈ Icc N (2 * N),
      ‖halaszPhaseMean F u k -
        (halaszPowerPhase u k / (1 + (-u : ℂ) * Complex.I)) * halaszPhaseMean F 0 k‖ ≤ E * k) :
    (∫ u in -U..U, ‖mrtDyadicPolynomial F N u‖ ^ 2) ≤
      50 * Real.pi * A ^ 2 + 100 * U * E ^ 2 := by
…

Mentions: OAI.TwoPointCorrelations.halaszPhaseMean, OAI.TwoPointCorrelations.halaszPowerPhase, OAI.TwoPointCorrelations.mrtDyadicPolynomial