HalaszFrequencyRows.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

A local frequency-mass estimate controls the entire quadratic-decay row. This keeps the prime-counting input separate from the finite harmonic-analysis argument, and applies to the actual finite Dirichlet polynomial.

def OAI.TwoPointCorrelations.halaszFrequencyShell line 14
Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszFrequencyRows.lean:14 (same declaration text).
lemma OAI.TwoPointCorrelations.halasz_quadratic_kernel_sum line 18
Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszFrequencyRows.lean:18 (same declaration text).
theorem OAI.TwoPointCorrelations.halasz_frequency_row_of_shells line 32
Source documentation
Shell mass at frequency resolution 1/T controls the whole Fourier kernel row, uniformly in the number and placement of the frequencies.
Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszFrequencyRows.lean:32 (same declaration text).
```
theorem halasz_frequency_row_of_shells {ι : Type*} (S : Finset ι)
    (freq w : ι → ℝ) (u : ℝ) {T B : ℝ} (hT : 0 < T) (hB : 0 ≤ B)
    (hw : ∀ i ∈ S, 0 ≤ w i)
    (hshell : ∀ k : ℕ, ∑ i ∈ halaszFrequencyShell S freq T u k, w i ≤ B / T) :
    (∑ i ∈ S, w i * (2 * T / (1 + T ^ 2 * (freq i - u) ^ 2))) ≤ 8 * B := by
…
```
Mentions: OAI.TwoPointCorrelations.halaszFrequencyShell

theorem OAI.TwoPointCorrelations.halasz_mean_square_of_frequency_shells line 83

Source documentation

The corresponding mean-square estimate for a finite polynomial whose weighted frequency shells all have controlled mass.

Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszFrequencyRows.lean:83 (same declaration text).

theorem halasz_mean_square_of_frequency_shells {ι : Type*} (S : Finset ι)
    (a : ι → ℂ) (w freq : ι → ℝ) {T B : ℝ} (hT : 0 < T) (hB : 0 ≤ B)
    (hw : ∀ i ∈ S, 0 ≤ w i)
    (hshell : ∀ i ∈ S, ∀ k : ℕ,
      ∑ j ∈ halaszFrequencyShell S freq T (freq i) k, w j ≤ B / T) :
    (∫ t in -T..T,
      ‖mrtExponentialPolynomial S (fun i => a i * (w i : ℂ)) freq t‖ ^ 2) ≤
      8 * Real.exp 1 * B * ∑ i ∈ S, ‖a i‖ ^ 2 * w i := by
…

Mentions: OAI.TwoPointCorrelations.halaszFrequencyShell, OAI.TwoPointCorrelations.mrtExponentialPolynomial

lemma OAI.TwoPointCorrelations.halasz_shell_mass_of_windows line 103

Source documentation

A shell is the union of its two one-sided frequency intervals.

Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszFrequencyRows.lean:103 (same declaration text).

lemma halasz_shell_mass_of_windows {ι : Type*} (S : Finset ι)
    (freq w : ι → ℝ) (u : ℝ) {T A : ℝ} (hT : 0 < T)
    (hw : ∀ i ∈ S, 0 ≤ w i)
    (hwindow : ∀ v : ℝ,
      (∑ i ∈ S.filter (fun i => v ≤ freq i ∧ freq i ≤ v + 1 / T), w i) ≤ A / T)
    (k : ℕ) :
    (∑ i ∈ halaszFrequencyShell S freq T u k, w i) ≤ 2 * A / T := by
…

Mentions: OAI.TwoPointCorrelations.halaszFrequencyShell

theorem OAI.TwoPointCorrelations.halasz_frequency_row_of_windows line 166

Source documentation

A uniform local frequency-mass bound gives a uniform kernel-row bound.

Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszFrequencyRows.lean:166 (same declaration text).

theorem halasz_frequency_row_of_windows {ι : Type*} (S : Finset ι)
    (freq w : ι → ℝ) (u : ℝ) {T A : ℝ} (hT : 0 < T) (hA : 0 ≤ A)
    (hw : ∀ i ∈ S, 0 ≤ w i)
    (hwindow : ∀ v : ℝ,
      (∑ i ∈ S.filter (fun i => v ≤ freq i ∧ freq i ≤ v + 1 / T), w i) ≤ A / T) :
    (∑ i ∈ S, w i * (2 * T / (1 + T ^ 2 * (freq i - u) ^ 2))) ≤ 16 * A := by
…