ShortFactorPowers.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Absorbing the explicit logarithmic factors in the short-polynomial moments, without making subpower growth an assumption.

lemma OAI.CubicFirstMoment.one_add_log_small_power line 12
lemma OAI.CubicFirstMoment.shortFactorPolynomial_norm_le line 22
theorem OAI.CubicFirstMoment.shortFactorPolynomial_norm_small_power line 37
theorem OAI.CubicFirstMoment.logarithmic_factor_product line 55
lemma OAI.CubicFirstMoment.half_power_absorb line 75

theorem OAI.CubicFirstMoment.shortFactor_multiplicity_power line 85

Source documentation

The exact short-factor cubic moments have the clean subpower-loss form used to extract the limiting multiplicity inequalities.

theorem shortFactor_multiplicity_power (k : ι → ℕ) {ε : ℝ} (hε : 0 < ε) :
    ∃ C : ℝ, 0 < C ∧ ∀ (F : ℝ) (X : ι → ℝ)
      (A : ι → EisensteinArithmeticFunction) (u : ι → Eisenstein → ℂ),
      (∀ i, ShortArithmeticFactor F (A i)) → (∀ i, 1 ≤ X i) →
      (∀ i, ∀ a ∈ primaryElementBall (X i), ‖u i a‖ ≤ 1) →
      ∀ (P : Finset Eisenstein) (N : ℝ), 1 ≤ N →
      (∀ a ∈ P, primary a ∧ Squarefree a ∧ norm a ≤ N) →
      (∑ a ∈ P, ‖∏ i,
        (primaryIdealPolynomial (X i) (A i) (fun n => u 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:ℝ)) := by
…

Mentions: OAI.CubicFirstMoment.EisensteinArithmeticFunction, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.ShortArithmeticFactor, OAI.CubicFirstMoment.primaryElementBall, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.primaryIdealPolynomial, OAI.CubicFirstMoment.cubicSymbol

theorem OAI.CubicFirstMoment.shortFactor_mixed_multiplicity_power line 132

Source documentation

The ordinary mixed moments have the same fully absorbed loss.

theorem shortFactor_mixed_multiplicity_power
    (hHuxley : HuxleyAdditiveLargeSieve) (k : ι → ℕ) {ε : ℝ} (hε : 0 < ε) :
    ∃ C : ℝ, 0 < C ∧ ∀ (F : ℝ) (X : ι → ℝ)
      (A : ι → EisensteinArithmeticFunction) (u : ι → Eisenstein → ℂ),
      (∀ i, ShortArithmeticFactor F (A i)) → (∀ i, 1 ≤ X i) →
      (∀ i, ∀ a ∈ primaryElementBall (X i), ‖u i a‖ ≤ 1) →
      ∀ (P : Finset (Eisenstein × Eisenstein)) (Q : ℝ), 1 ≤ Q →
      (∀ p ∈ P, PrimarySquarefreePair p ∧ norm (pairConductor p) ≤ Q) →
      (∑ p ∈ P, ‖∏ i, (primaryIdealPolynomial (X i) (A i)
        (fun n => u i n*mixedCubic p.1 p.2 n))^(k i)‖^2) ≤
        C*(Q*(∏ i, (X i)^(k i)))^ε*(∏ i, (X i)^(k i))*
          (Q^2+(∏ i, (X i)^(k i))) := by
…

Mentions: OAI.CubicFirstMoment.HuxleyAdditiveLargeSieve, OAI.CubicFirstMoment.EisensteinArithmeticFunction, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.ShortArithmeticFactor, OAI.CubicFirstMoment.primaryElementBall, OAI.CubicFirstMoment.PrimarySquarefreePair, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.pairConductor, OAI.CubicFirstMoment.primaryIdealPolynomial, OAI.CubicFirstMoment.mixedCubic