Documentation

LeanPool.KrafftSieve.Variance

Sieve Variance #

This module defines the mean density $\mu$ and the physical variance $\sigma^2$ of the survivor distribution in the Krafft Sieve, and proves Parseval's identity to relate the variance to the Fourier coefficients.

source
def KrafftSieve.N (n : ℕ) (r : Fin (w n) → ℕ) :
ℕ

Definition of N as the cardinality of A. Let $N = |A| = \prod_{i=1}^w (p_i - 2)$ be the total number of surviving residues.

Equations
Instances For
    source
    noncomputable def KrafftSieve.μ (n : ℕ) (r : Fin (w n) → ℕ) :
    ℝ

    Definition of the global mean density μ. Define the global mean density $\mu = \frac{N}{q}$.

    Equations
    Instances For
      source
      noncomputable def KrafftSieve.fHat (n : ℕ) (r : Fin (w n) → ℕ) (h : ZMod (q n)) :
      ℂ

      Definition of the Discrete Fourier Transform fHat. Define the Discrete Fourier Transform of $f$ at frequency $h \in \mathbb{Z}/q\mathbb{Z}$ as: $$ \hat{f}(h) = \frac{1}{q} \sum_{x=0}^{q-1} f(x) e^{-2\pi i h x / q} $$

      Equations
      Instances For
        source
        noncomputable def KrafftSieve.sigmaSq (n : ℕ) (r : Fin (w n) → ℕ) :
        ℝ

        Definition of the physical variance sigmaSq. Define the physical variance of the survivor distribution as: $$ \sigma^2 = \frac{1}{q} \sum_{x=0}^{q-1} (f(x) - \mu)^2 $$

        Equations
        Instances For
          source
          theorem KrafftSieve.f_hat_zero_eq_mu (n : ℕ) (r : Fin (w n) → ℕ) :
          fHat n r 0 = ↑(μ n r)

          The Fourier coefficient at 0 is equal to the mean density μ.

          source
          theorem KrafftSieve.sum_exp_orthogonality (n : ℕ) (k : ZMod (q n)) :
          ∑ h : ZMod (q n), Complex.exp (2 * ↑Real.pi * Complex.I * ↑h.val * ↑k.val / ↑(q n)) = if k = 0 then ↑(q n) else 0

          Orthogonality of the exponential sum.

          source
          theorem KrafftSieve.orthogonality_x (n : ℕ) (k : ZMod (q n)) :
          ∑ x : ZMod (q n), Complex.exp (2 * ↑Real.pi * Complex.I * ↑k.val * ↑x.val / ↑(q n)) = if k = 0 then ↑(q n) else 0

          Orthogonality of the exponential sum over $x$.

          source
          theorem KrafftSieve.sum_orthogonality_application (n : ℕ) (r : Fin (w n) → ℕ) :
          ∑ x : ZMod (q n), ∑ y : ZMod (q n), ↑(f n r x) * ↑(f n r y) * ∑ h : ZMod (q n), Complex.exp (2 * ↑Real.pi * Complex.I * ↑h.val * ↑(y - x).val / ↑(q n)) = ↑(q n) * ∑ x : ZMod (q n), ↑(f n r x) ^ 2

          Application of orthogonality to simplify the double sum of function values.

          source
          theorem KrafftSieve.f_hat_normSq_expansion (n : ℕ) (r : Fin (w n) → ℕ) (h : ZMod (q n)) :
          ↑(Complex.normSq (fHat n r h)) = 1 / ↑(q n) ^ 2 * ∑ x : ZMod (q n), ∑ y : ZMod (q n), ↑(f n r x) * ↑(f n r y) * Complex.exp (2 * ↑Real.pi * Complex.I * ↑h.val * ↑(y - x).val / ↑(q n))

          Expansion of the squared magnitude of a single Fourier coefficient.

          source
          theorem KrafftSieve.parseval_standard (n : ℕ) (r : Fin (w n) → ℕ) :
          ∑ h : ZMod (q n), Complex.normSq (fHat n r h) = 1 / ↑(q n) * ∑ x : ZMod (q n), f n r x ^ 2

          Standard Parseval's Identity: The sum of the squared magnitudes of the Fourier coefficients equals the average of the squared function values.

          source
          theorem KrafftSieve.variance_expansion (n : ℕ) (r : Fin (w n) → ℕ) :
          sigmaSq n r = 1 / ↑(q n) * ∑ x : ZMod (q n), f n r x ^ 2 - μ n r ^ 2

          Expansion of the variance formula.

          source
          theorem KrafftSieve.parseval_identity (n : ℕ) (r : Fin (w n) → ℕ) :
          sigmaSq n r = ∑ h : ZMod (q n), if h = 0 then 0 else Complex.normSq (fHat n r h)

          Parseval's Identity for the Sieve: The variance of the indicator function f is strictly equal to the sum of the squared magnitudes of its non-zero Fourier coefficients.

          source
          theorem KrafftSieve.q_odd (n : ℕ) :
          Odd (q n)

          The primorial $q$ is odd.

          source
          theorem KrafftSieve.f_hat_conj_symm (n : ℕ) (r : Fin (w n) → ℕ) (h : ZMod (q n)) :
          fHat n r (-h) = (starRingEnd ℂ) (fHat n r h)

          Conjugate symmetry of the Fourier transform for real-valued functions.

          source
          theorem KrafftSieve.harmonic_variance_lower_bound (n : ℕ) (r : Fin (w n) → ℕ) (h : ZMod (q n)) (h_ne_zero : h ≠ 0) :
          sigmaSq n r ≥ 2 * Complex.normSq (fHat n r h)

          Harmonic Variance Lower Bound: For any non-zero frequency $h$, the variance is at least twice the squared magnitude of the Fourier coefficient at $h$.