Optimal Weights

This module constructs the truly multidimensional optimal weights $\lambda$ for the Krafft Sieve and explores the properties of the resulting polynomial $P(x)$ and weight $W_\lambda(x)$.

noncomputable def KrafftSieve.basisCos (n : ℕ) (S : Finset (Fin (w n))) (x : ZMod (q n)) : ℝ

Define the basis function for a subset of prime indices $S \subseteq \{1, \dots, w\}$. The basis function is the product of the 3rd harmonic cosines for each prime in $S$. $$ B_S(x) = \prod_{i \in S} \cos\left( \frac{6\pi x}{p_i} \right) $$

Equations

• KrafftSieve.basisCos n S x = ∏ i ∈ S, Real.cos (2 * Real.pi * 3 * ↑x.val / ↑(KrafftSieve.p n i))

noncomputable def KrafftSieve.pMulti (n : ℕ) (lambda : Finset (Fin (w n)) → ℝ) (x : ZMod (q n)) : ℝ

Define the multidimensional polynomial $P(x)$ as a linear combination of the basis functions $B_S(x)$ with coefficients $\lambda_S$. $$ P(x) = \sum_{S \subseteq \{1, \dots, w\}} \lambda_S B_S(x) $$

Equations

• KrafftSieve.pMulti n lambda x = ∑ S ∈ Finset.univ.powerset, lambda S * KrafftSieve.basisCos n S x

noncomputable def KrafftSieve.wTrulyMulti (n : ℕ) (lambda : Finset (Fin (w n)) → ℝ) (x : ZMod (q n)) : ℝ

Define the truly multidimensional weight function $W_{\lambda}(x)$ as the square of the polynomial $P(x)$ restricted to the interval $\mathcal{A}_n$. $$ W_{\lambda}(x) = \begin{cases} (P(x))^2 & \text{if } x \in \mathcal{A}_n \\ 0 & \text{otherwise} \end{cases} $$

Equations

• KrafftSieve.wTrulyMulti n lambda x = if x.val ∈ KrafftSieve.evalInterval n then KrafftSieve.pMulti n lambda x ^ 2 else 0

noncomputable def KrafftSieve.matrix1 (n : ℕ) (S T : Finset (Fin (w n))) : ℝ

Define the matrix $M_1$ corresponding to the first moment $sum1$. $M_1(S, T) = \sum_{x \in \mathcal{A}_n} B_S(x) B_T(x)$

Equations

• KrafftSieve.matrix1 n S T = ∑ x ∈ KrafftSieve.evalInterval n, KrafftSieve.basisCos n S ↑x * KrafftSieve.basisCos n T ↑x

noncomputable def KrafftSieve.matrix2 (n : ℕ) (S T : Finset (Fin (w n))) : ℝ

Define the matrix $M_2$ corresponding to the second moment $sum2$. $M_2(S, T) = \sum_{x \in \mathcal{A}_n} c(x) B_S(x) B_T(x)$

Equations

• KrafftSieve.matrix2 n S T = ∑ x ∈ KrafftSieve.evalInterval n, KrafftSieve.c n ↑x * KrafftSieve.basisCos n S ↑x * KrafftSieve.basisCos n T ↑x

noncomputable def KrafftSieve.q1 (n : ℕ) (lambda : Finset (Fin (w n)) → ℝ) : ℝ

Define the quadratic form $q1(\lambda) = \lambda^T M_1 \lambda$.

Equations

• KrafftSieve.q1 n lambda = ∑ S ∈ Finset.univ.powerset, ∑ T ∈ Finset.univ.powerset, lambda S * KrafftSieve.matrix1 n S T * lambda T

noncomputable def KrafftSieve.q2 (n : ℕ) (lambda : Finset (Fin (w n)) → ℝ) : ℝ

Define the quadratic form $q2(\lambda) = \lambda^T M_2 \lambda$.

Equations

• KrafftSieve.q2 n lambda = ∑ S ∈ Finset.univ.powerset, ∑ T ∈ Finset.univ.powerset, lambda S * KrafftSieve.matrix2 n S T * lambda T

noncomputable def KrafftSieve.Ratio (n : ℕ) (lambda : Finset (Fin (w n)) → ℝ) : ℝ

Define the Rayleigh quotient $R(\lambda) = \frac{q2(\lambda)}{q1(\lambda)}$. Defined to be $\infty$ if $q1(\lambda) = 0$ (though $q1$ is positive definite on non-zero $\lambda$ if the basis is linearly independent on $evalInterval$).

Equations

• KrafftSieve.Ratio n lambda = if KrafftSieve.q1 n lambda = 0 then 0 else KrafftSieve.q2 n lambda / KrafftSieve.q1 n lambda

theorem KrafftSieve.W_truly_multi_nonneg (n : ℕ) (lambda : Finset (Fin (w n)) → ℝ) (x : ZMod (q n)) : wTrulyMulti n lambda x ≥ 0

The truly multidimensional weight function is non-negative everywhere.

theorem KrafftSieve.W_truly_multi_support (n : ℕ) (lambda : Finset (Fin (w n)) → ℝ) (x : ZMod (q n)) (hx : x.val ∉ evalInterval n) : wTrulyMulti n lambda x = 0

The truly multidimensional weight function is supported on $\mathcal{A}_n$.

theorem KrafftSieve.S_1_eq_Q_1 (n : ℕ) (lambda : Finset (Fin (w n)) → ℝ) : sum1 n (wTrulyMulti n lambda) = q1 n lambda

Lemma: The first moment $sum1$ of the truly multidimensional weight is equal to the quadratic form $q1$.

theorem KrafftSieve.S_2_eq_Q_2 (n : ℕ) (lambda : Finset (Fin (w n)) → ℝ) : sum2 n (wTrulyMulti n lambda) = q2 n lambda

Lemma: The second moment $sum2$ of the truly multidimensional weight is equal to the quadratic form $q2$.

theorem KrafftSieve.sufficiency_of_Q (n : ℕ) (lambda : Finset (Fin (w n)) → ℝ) (h : q2 n lambda < q1 n lambda) : KrafftSufficiency n

Lemma: The existence of coefficients $\lambda$ such that $q2(\lambda) < q1(\lambda)$ is sufficient for Krafft Sufficiency.

def KrafftSieve.attainableRatios (n : ℕ) : Set ℝ

Define the set of attainable ratios.

Equations

• KrafftSieve.attainableRatios n = {r : ℝ | ∃ (lambda : Finset (Fin (KrafftSieve.w n)) → ℝ), KrafftSieve.q1 n lambda > 0 ∧ r = KrafftSieve.Ratio n lambda}

noncomputable def KrafftSieve.muMin (n : ℕ) : ℝ

Define $\mu_{min}(n)$ as the infimum of the attainable ratios.

Equations

• KrafftSieve.muMin n = sInf (KrafftSieve.attainableRatios n)

theorem KrafftSieve.mu_min_lt_one_implies_sufficiency (n : ℕ) (h : muMin n < 1) : KrafftSufficiency n

Theorem: If the minimum attainable ratio $\mu_{min}(n)$ is strictly less than 1, then the Krafft Sufficiency condition holds.

@[reducible, inline]

abbrev KrafftSieve.Idx (n : ℕ) : Type

Abbreviation for the index set of the coefficients, which is the power set of prime indices.

Equations

• KrafftSieve.Idx n = Finset (Fin (KrafftSieve.w n))

def KrafftSieve.kernelQ1 (n : ℕ) : Submodule ℝ (Idx n → ℝ)

The kernel of the quadratic form $q1$.

Equations

• KrafftSieve.kernelQ1 n = { carrier := {lambda : KrafftSieve.Idx n → ℝ | KrafftSieve.q1 n lambda = 0}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

theorem KrafftSieve.Q_1_eq_zero_iff (n : ℕ) (lambda : Idx n → ℝ) : q1 n lambda = 0 ↔ ∀ x ∈ evalInterval n, pMulti n lambda ↑x = 0

Lemma: $q1(\lambda) = 0$ if and only if $P_{multi}(\lambda, x) = 0$ for all $x \in \mathcal{A}_n$.

theorem KrafftSieve.Q_1_nonneg (n : ℕ) (lambda : Idx n → ℝ) : q1 n lambda ≥ 0

Lemma: $q1$ is non-negative for all $\lambda$.

def KrafftSieve.dotProduct (n : ℕ) (u v : Idx n → ℝ) : ℝ

Define the standard dot product on the space of coefficients.

Equations

• KrafftSieve.dotProduct n u v = ∑ S : KrafftSieve.Idx n, u S * v S

def KrafftSieve.kernelQ1Perp (n : ℕ) : Submodule ℝ (Idx n → ℝ)

The orthogonal complement of the kernel of $q1$ with respect to the standard dot product.

Equations

• KrafftSieve.kernelQ1Perp n = { carrier := {v : KrafftSieve.Idx n → ℝ | ∀ u ∈ KrafftSieve.kernelQ1 n, KrafftSieve.dotProduct n u v = 0}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

def KrafftSieve.spherePerp (n : ℕ) : Set (Idx n → ℝ)

The unit sphere in the orthogonal complement of the kernel of $q1$.

Equations

• KrafftSieve.spherePerp n = {lambda : KrafftSieve.Idx n → ℝ | lambda ∈ KrafftSieve.kernelQ1Perp n ∧ KrafftSieve.dotProduct n lambda lambda = 1}

theorem KrafftSieve.Q_1_pos_on_sphere_perp (n : ℕ) (lambda : Idx n → ℝ) (h : lambda ∈ spherePerp n) : q1 n lambda > 0

Lemma: $q1$ is strictly positive on the unit sphere of the orthogonal complement.

theorem KrafftSieve.Q_1_not_zero (n : ℕ) : ∃ (lambda : Idx n → ℝ), q1 n lambda ≠ 0

Lemma: $q1$ is not identically zero.

theorem KrafftSieve.Ratio_scale (n : ℕ) (lambda : Idx n → ℝ) (c : ℝ) (hc : c ≠ 0) : Ratio n (c • lambda) = Ratio n lambda

Lemma: The Rayleigh quotient is scale-invariant.

theorem KrafftSieve.sq_le_dot_product (n : ℕ) (v : Idx n → ℝ) (i : Idx n) : v i ^ 2 ≤ dotProduct n v v

Lemma: For any vector $v$, the square of any component is bounded by the dot product.

theorem KrafftSieve.decomposition (n : ℕ) (x : Idx n → ℝ) : ∃ u ∈ kernelQ1 n, ∃ v ∈ kernelQ1Perp n, x = u + v

Lemma: Any vector can be decomposed into a component in the kernel of $q1$ and a component in the orthogonal complement.

theorem KrafftSieve.P_multi_add (n : ℕ) (u v : Idx n → ℝ) (x : ZMod (q n)) : pMulti n (u + v) x = pMulti n u x + pMulti n v x

Lemma: The polynomial $P_{multi}$ is linear in $\lambda$.

theorem KrafftSieve.sphere_perp_compact (n : ℕ) : IsCompact (spherePerp n)

Lemma: The unit sphere in the orthogonal complement is compact.

theorem KrafftSieve.Q_2_add_kernel (n : ℕ) (u v : Idx n → ℝ) (hu : u ∈ kernelQ1 n) : q2 n (u + v) = q2 n v

Lemma: If $u \in \text{kernel}(q1)$, then $q2(u + v) = q2(v)$.

theorem KrafftSieve.Ratio_add_kernel (n : ℕ) (u v : Idx n → ℝ) (hu : u ∈ kernelQ1 n) : Ratio n (u + v) = Ratio n v

Lemma: The Rayleigh quotient is invariant under adding a vector from the kernel of $q1$.

theorem KrafftSieve.exists_sphere_perp_ratio_eq (n : ℕ) (lambda : Idx n → ℝ) (hQ1 : q1 n lambda > 0) : ∃ v ∈ spherePerp n, Ratio n lambda = Ratio n v

Lemma: For any $\lambda$ with $q1(\lambda) > 0$, there exists $v \in \text{sphere\_perp}(n)$ such that $\text{Ratio}(n, \lambda) = \text{Ratio}(n, v)$.

theorem KrafftSieve.attainable_ratios_eq_image_sphere_perp (n : ℕ) : attainableRatios n = Ratio n '' spherePerp n

Lemma: The set of attainable ratios is the image of the unit sphere in the orthogonal complement under the Rayleigh quotient map.

theorem KrafftSieve.attainable_ratios_compact (n : ℕ) : IsCompact (attainableRatios n)

Lemma: The set of attainable ratios is compact.

theorem KrafftSieve.exists_minimizer (n : ℕ) : ∃ (lambda : Idx n → ℝ), q1 n lambda > 0 ∧ Ratio n lambda = muMin n

Lemma: The minimum attainable ratio is attained by some coefficient vector $\lambda$.

noncomputable def KrafftSieve.lambdaOpt (n : ℕ) : Idx n → ℝ

Define the optimal coefficient vector $\lambda_{opt}$ which attains the minimum ratio.

Equations

• KrafftSieve.lambdaOpt n = ⋯.choose

theorem KrafftSieve.lambda_opt_spec (n : ℕ) : q1 n (lambdaOpt n) > 0 ∧ Ratio n (lambdaOpt n) = muMin n

Properties of the optimal coefficient vector.

noncomputable def KrafftSieve.wOpt (n : ℕ) : ZMod (q n) → ℝ

Define the optimal truly multidimensional weight function $W_{opt}$.

Equations

• KrafftSieve.wOpt n = KrafftSieve.wTrulyMulti n (KrafftSieve.lambdaOpt n)

theorem KrafftSieve.W_opt_is_sufficient_iff (n : ℕ) : sum2 n (wOpt n) < sum1 n (wOpt n) ↔ muMin n < 1

Theorem: The optimal weight function satisfies the Krafft Sufficiency condition if and only if $\mu_{min}(n) < 1$.

theorem KrafftSieve.krafft_sieve_guarantee_with_mu_min (n : ℕ) (h : muMin n < 1) : ∃ x ∈ evalInterval n, Nat.Prime (6 * x - 1) ∧ Nat.Prime (6 * x + 1)

Theorem: The Krafft Sieve Guarantee holds if $\mu_{min}(n) < 1$.