FourierPrimeCutoff.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Fourier inversion of a cutoff evaluated at the centered count of distinct prime divisors. The integral kernel splits into a constant phase and the multiplicative finite-prime twist.

def OAI.TwoPointCorrelations.primeCutoffKernel line 16
lemma OAI.TwoPointCorrelations.norm_primeCutoffKernel line 19
lemma OAI.TwoPointCorrelations.primeCutoffKernel_eq_exp line 24
lemma OAI.TwoPointCorrelations.continuous_primeCutoffKernel line 34
lemma OAI.TwoPointCorrelations.integrable_weighted_primeCutoffKernel line 39
def OAI.TwoPointCorrelations.primeCountCutoff line 45
lemma OAI.TwoPointCorrelations.primeCountCutoff_eq_fourierInv line 49
theorem OAI.TwoPointCorrelations.primeCountCutoff_fourier line 64
Source documentation
This is the actual cutoff φ((ω_P(n)-μ)/σ) when the frequency coefficient is the Fourier transform of a continuous integrable cutoff.
```
theorem primeCountCutoff_fourier (P : Finset ℕ) (μ σ : ℝ)
    (φ : ℝ → ℂ) (hφ : Continuous φ) (hi : Integrable φ)
    (hFourier : Integrable (𝓕 φ)) (n : ℕ) :
    primeCountCutoff P μ σ (𝓕 φ) n =
      φ (((finitePrimeDivisorCount P n : ℝ) - μ) / σ) := by
…
```
Mentions: OAI.TwoPointCorrelations.primeCountCutoff, OAI.TwoPointCorrelations.finitePrimeDivisorCount

theorem OAI.TwoPointCorrelations.primeCountCutoff_pair_sum line 73

Source documentation

Exact interchange for the two prime-count cutoffs in a finite correlation sum.

theorem primeCountCutoff_pair_sum {ι : Type*} (S : Finset ι) (c : ι → ℂ)
    (n m : ι → ℕ) (P Q : Finset ℕ) (μ σ ν τ : ℝ) (w₁ w₂ : ℝ → ℂ)
    (hw₁ : Integrable w₁) (hw₂ : Integrable w₂) :
    (∑ i ∈ S, c i * primeCountCutoff P μ σ w₁ (n i) *
      primeCountCutoff Q ν τ w₂ (m i)) =
      ∫ t, ∫ s, ∑ i ∈ S,
        c i * (w₁ t * primeCutoffKernel P μ σ t (n i)) *
          (w₂ s * primeCutoffKernel Q ν τ s (m i)) := by
…

Mentions: OAI.TwoPointCorrelations.primeCountCutoff, OAI.TwoPointCorrelations.primeCutoffKernel

theorem OAI.TwoPointCorrelations.primeCountCutoff_twisted_pair_sum line 89

Source documentation

The cutoff factors are exactly a Fourier average of multiplicative finite-prime twists, with two unit-modulus constant phases.

theorem primeCountCutoff_twisted_pair_sum {ι : Type*} (S : Finset ι)
    (c : ι → ℂ) (n m : ι → ℕ) (f g : ℕ → ℂ) (P Q : Finset ℕ)
    (μ σ ν τ : ℝ) (w₁ w₂ : ℝ → ℂ)
    (hw₁ : Integrable w₁) (hw₂ : Integrable w₂) :
    (∑ i ∈ S, (c i * f (n i) * g (m i)) * primeCountCutoff P μ σ w₁ (n i) *
      primeCountCutoff Q ν τ w₂ (m i)) =
      ∫ t, ∫ s, w₁ t * w₂ s *
        (additiveCharacter (-t * μ / σ) 1 * additiveCharacter (-s * ν / τ) 1 *
          ∑ i ∈ S, c i * twistByPrimePhase f P (t / σ) (n i) *
            twistByPrimePhase g Q (s / τ) (m i)) := by
…

Mentions: OAI.TwoPointCorrelations.primeCountCutoff, OAI.TwoPointCorrelations.additiveCharacter, OAI.TwoPointCorrelations.twistByPrimePhase

theorem OAI.TwoPointCorrelations.norm_primeCountCutoff_pair_sum_le line 113