PrimaryMultiplicity.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Actual fixed multiplicities in the exceptional-moment argument.

lemma OAI.CubicFirstMoment.prod_fixed_copies line 13
lemma OAI.CubicFirstMoment.fixed_copies_norm_bound line 19

theorem OAI.CubicFirstMoment.primaryPolynomial_multiplicity_moment line 34

Source documentation

Every fixed multiplicity vector gives the actual power product of the primary polynomials, with the sharp cubic-sieve length factor.

theorem primaryPolynomial_multiplicity_moment (k : ι → ℕ)
    {ε δ : ℝ} (hε : 0 < ε) (hδ : 0 < δ) :
    ∃ C : ℝ, 0 < C ∧ ∀ (S : ι → Finset Eisenstein)
      (w : ι → Eisenstein → ℂ) (M X : ι → ℝ),
      (∀ i, ∀ a ∈ S i, primary a) → (∀ i, 0 ≤ M i) →
      (∀ i, ∀ a ∈ S i, ‖w i a‖ ≤ M i) → (∀ i, 1 ≤ X i) →
      (∀ i, ∀ a ∈ S i, norm a ≤ X i) →
      ∀ (P : Finset Eisenstein) (N : ℝ), 1 ≤ N →
      (∀ a ∈ P, primary a ∧ Squarefree a ∧ norm a ≤ N) →
      (∑ a ∈ P, ‖∏ i, (∑ n ∈ S i, w i n*cubicSymbol a n)^(k i)‖^2) ≤
        C*(N*(∏ i, (X i)^(k i)))^ε*(∏ i, (X i)^(k i))*
          (N+(∏ i, (X i)^(k i))+(N*(∏ i, (X i)^(k i)))^(2/3:ℝ))*
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.cubicSymbol

theorem OAI.CubicFirstMoment.primaryPolynomial_mixed_multiplicity_moment line 62

Source documentation

The same fixed copies in the ordinary mixed-character sieve retain the exact product of quadratic factor energies.

theorem primaryPolynomial_mixed_multiplicity_moment
    (hHuxley : HuxleyAdditiveLargeSieve) (k : ι → ℕ)
    {ε δ : ℝ} (hε : 0 < ε) (hδ : 0 < δ) :
    ∃ C : ℝ, 0 < C ∧ ∀ (S : ι → Finset Eisenstein)
      (w : ι → Eisenstein → ℂ) (X : ι → ℝ),
      (∀ i, ∀ a ∈ S i, primary a) → (∀ i, 1 ≤ X i) →
      (∀ i, ∀ a ∈ S i, norm a ≤ X i) →
      ∀ (P : Finset (Eisenstein × Eisenstein)) (Q : ℝ), 1 ≤ Q →
      (∀ p ∈ P, PrimarySquarefreePair p ∧ norm (pairConductor p) ≤ Q) →
      (∑ p ∈ P, ‖∏ i, (∑ n ∈ S i, w i n*mixedCubic p.1 p.2 n)^(k i)‖^2) ≤
        C*Q^ε*(Q^2+(∏ i, (X i)^(k i)))*
          ((∏ i, (X i)^(k i))^δ*(∏ i, (∑ n ∈ S i, ‖w i n‖^2)^(k i))) := by
…

Mentions: OAI.CubicFirstMoment.HuxleyAdditiveLargeSieve, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.PrimarySquarefreePair, OAI.CubicFirstMoment.pairConductor, OAI.CubicFirstMoment.mixedCubic