The actual finite-dimensional Stepanov equations

The two polynomial families have degree strictly less than the integer B. The kth equation is Harcos (22), with its two distinct Hasse operators. No rank or nonzero-solution hypothesis is imposed on the equation matrix.

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stepanovConstraint {F : Type u_1} [Field F] (f : Polynomial F) (hf : f ≠ 0) (ell e : ℕ) (a : F) (k : ℕ) {J : ℕ} (r s : Fin J → Polynomial F) : Polynomial F

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stepanovConstraint f hf ell e a k r s = ∑ j : Fin J, ((MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stepanovHasseOperator f hf ell k) (r j) + a • (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stepanovHasseOperator f hf (ell + e) k) (s j)) * Polynomial.X ^ ↑j

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stepanovConstraint_degree_lt {F : Type u_1} [Field F] (f : Polynomial F) (hf : f ≠ 0) (ell e B J k : ℕ) (a : F) (hk : k ≤ ell) (hm : 1 ≤ f.natDegree) (hJ : 0 < J) (r s : Fin J → Polynomial F) (hr : ∀ (j : Fin J), (r j).degree < ↑B) (hs : ∀ (j : Fin J), (s j).degree < ↑B) : (stepanovConstraint f hf ell e a k r s).degree < ↑(B + k * (f.natDegree - 1) + (J - 1))

@[reducible, inline]

abbrev MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.StepanovCoefficients (F : Type u_2) [Field F] (J B : ℕ) : Type u_2

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.StepanovCoefficients F J B = (Fin J → ↥(Polynomial.degreeLT F B) × ↥(Polynomial.degreeLT F B))

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stepanovConstraintMap {F : Type u_1} [Field F] (f : Polynomial F) (hf : f ≠ 0) (ell e B J : ℕ) (a : F) (hm : 1 ≤ f.natDegree) (hJ : 0 < J) : StepanovCoefficients F J B →ₗ[F] (k : Fin ell) → ↥(Polynomial.degreeLT F (B + ↑k * (f.natDegree - 1) + (J - 1)))

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stepanovConstraintMap f hf ell e B J a hm hJ = { toFun := fun (v : MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.StepanovCoefficients F J B) (k : Fin ell) => ⟨MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stepanovConstraint f hf ell e a (↑k) (fun (j : Fin J) => ↑(v j).1) fun (j : Fin J) => ↑(v j).2, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stepanovCoefficients_finrank {F : Type u_1} [Field F] (J B : ℕ) : Module.finrank F (StepanovCoefficients F J B) = 2 * J * B

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stepanovConstraints_finrank {F : Type u_1} [Field F] (ell B J m : ℕ) : Module.finrank F ((k : Fin ell) → ↥(Polynomial.degreeLT F (B + ↑k * (m - 1) + (J - 1)))) = ∑ k : Fin ell, (B + ↑k * (m - 1) + (J - 1))

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stepanov_exists_coefficients {F : Type u_1} [Field F] (f : Polynomial F) (hf : f ≠ 0) (ell e B J : ℕ) (a : F) (hm : 1 ≤ f.natDegree) (hJ : 0 < J) (hcount : ∑ k : Fin ell, (B + ↑k * (f.natDegree - 1) + (J - 1)) < 2 * J * B) : ∃ (r : Fin J → Polynomial F) (s : Fin J → Polynomial F), (∀ (j : Fin J), (r j).degree < ↑B) ∧ (∀ (j : Fin J), (s j).degree < ↑B) ∧ (∃ (j : Fin J), r j ≠ 0 ∨ s j ≠ 0) ∧ ∀ k < ell, stepanovConstraint f hf ell e a k r s = 0

The precise integer equation count, strictly smaller than the 2JB unknown coefficients, produces a nontrivial solution of Harcos (22).