RoughFourier.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

Exact finite Fourier identities for rough shifts

Orthogonality, convolution and the fourth moment are proved for arbitrary finite coefficients. The sieve bounds on the number of rough integers are not hypotheses of these identities. Haar measure on AddCircle (1 : ℝ) is the ordinary integral over one period.

def OAI.TwoPointCorrelations.fourierPolynomial line 20
theorem OAI.TwoPointCorrelations.continuous_fourierPolynomial line 24
theorem OAI.TwoPointCorrelations.integral_circle_eq_period line 31
theorem OAI.TwoPointCorrelations.integral_fourier_character line 37
theorem OAI.TwoPointCorrelations.integrable_fourier_character line 43
theorem OAI.TwoPointCorrelations.integral_fourierPolynomial line 49
theorem OAI.TwoPointCorrelations.norm_fourierPolynomial_le line 62
theorem OAI.TwoPointCorrelations.fourierPolynomial_mul line 70
theorem OAI.TwoPointCorrelations.fourierPolynomial_conj line 85

theorem OAI.TwoPointCorrelations.integral_fourier_product line 92

Source documentation

Exact Fourier selection of all frequency-zero terms in a product.

theorem integral_fourier_product {ι κ : Type*} (S : Finset ι) (T : Finset κ)
    (f : ι → ℤ) (g : κ → ℤ) (a : ι → ℂ) (b : κ → ℂ) :
    (∫ θ, fourierPolynomial S f a θ * fourierPolynomial T g b θ
        ∂AddCircle.haarAddCircle) =
      ∑ i ∈ S ×ˢ T, if f i.1 + g i.2 = 0 then a i.1 * b i.2 else 0 := by
…

Mentions: OAI.TwoPointCorrelations.fourierPolynomial

theorem OAI.TwoPointCorrelations.integral_norm_fourierPolynomial_sq line 101

Source documentation

Parseval for finite polynomials, retaining collisions of frequencies.

theorem integral_norm_fourierPolynomial_sq {ι : Type*} (S : Finset ι)
    (f : ι → ℤ) (a : ι → ℂ) :
    (∫ θ, ‖fourierPolynomial S f a θ‖ ^ 2 ∂AddCircle.haarAddCircle) =
      ∑ i ∈ S ×ˢ S, if f i.1 = f i.2 then (a i.1 * conj (a i.2)).re else 0 := by
…

Mentions: OAI.TwoPointCorrelations.fourierPolynomial

theorem OAI.TwoPointCorrelations.integral_norm_fourierPolynomial_fourth line 120

Source documentation

The exact weighted additive-energy identity. In particular a positive integer dilation of the frequencies leaves its additive relation unchanged.

theorem integral_norm_fourierPolynomial_fourth {ι : Type*} (S : Finset ι)
    (f : ι → ℤ) (a : ι → ℂ) :
    (∫ θ, ‖fourierPolynomial S f a θ‖ ^ 4 ∂AddCircle.haarAddCircle) =
      ∑ i ∈ (S ×ˢ S) ×ˢ (S ×ˢ S),
        if f i.1.1 + f i.1.2 = f i.2.1 + f i.2.2 then
          (a i.1.1 * a i.1.2 * conj (a i.2.1 * a i.2.2)).re else 0 := by
…

Mentions: OAI.TwoPointCorrelations.fourierPolynomial

def OAI.TwoPointCorrelations.roughFourierPolynomial line 136
Source documentation
The actual polynomial in (q:rough-fourier).
```
noncomputable def roughFourierPolynomial (Z : Finset ℕ) (h : ℕ) : AddCircle (1 : ℝ) → ℂ :=
…
```
theorem OAI.TwoPointCorrelations.norm_roughFourierPolynomial_le line 139

theorem OAI.TwoPointCorrelations.roughFourierPolynomial_fourth_moment line 152

Source documentation

Weighted additive energy, without any sieve hypothesis.

theorem roughFourierPolynomial_fourth_moment (Z : Finset ℕ) (h : ℕ) (hh : 0 < h) :
    (∫ θ, ‖roughFourierPolynomial Z h θ‖ ^ 4 ∂AddCircle.haarAddCircle) =
      ∑ i ∈ ((Z ×ˢ Z) ×ˢ (Z ×ˢ Z)).filter
          (fun i => i.1.1 + i.1.2 = i.2.1 + i.2.2),
        (i.1.1 : ℝ)⁻¹ * (i.1.2 : ℝ)⁻¹ * (i.2.1 : ℝ)⁻¹ * (i.2.2 : ℝ)⁻¹ := by
…

Mentions: OAI.TwoPointCorrelations.roughFourierPolynomial

theorem OAI.TwoPointCorrelations.roughFourierPolynomial_fourth_moment_le line 173

Source documentation

A triple/quadruple count enters the fourth moment only through this explicit positive weight estimate.

theorem roughFourierPolynomial_fourth_moment_le (Z : Finset ℕ) (h : ℕ) (hh : 0 < h)
    (D : ℝ) (hD : 0 < D) (hZ : ∀ z ∈ Z, D ≤ (z : ℝ)) :
    (∫ θ, ‖roughFourierPolynomial Z h θ‖ ^ 4 ∂AddCircle.haarAddCircle) ≤
      (((Z ×ˢ Z) ×ˢ (Z ×ˢ Z)).filter
        (fun i => i.1.1 + i.1.2 = i.2.1 + i.2.2)).card * (D⁻¹) ^ 4 := by
…

Mentions: OAI.TwoPointCorrelations.roughFourierPolynomial