OAI/NumberTheory/CubicMoment/Estimates/PrimePowerBalanced.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CubicFirstMoment.balancedPrimePower_power line 10
2. theorem OAI.CubicFirstMoment.boundedPrimeSupport_balanced_sparse_moment line 41

   Source documentation

   The sparse coefficient energy and the bounded number of prime bases suffice for the actual balanced mixed-character second moment.

   theorem boundedPrimeSupport_balanced_sparse_moment
       (hHuxley : HuxleyAdditiveLargeSieve) (k : ℕ) {θ : ℝ}
       (hθ : 0 < θ) (hθ₁ : θ ≤ 1) :
       ∃ C : ℝ, 0 < C ∧ ∀ (Y E : ℝ), 1 ≤ Y → 0 ≤ E →
         ∀ B : Finset Eisenstein,
         (∀ b ∈ B, primary b ∧ norm b ≤ Y ∧ (idealExponentOf b).support.card ≤ k) →
         ∀ P : Finset (Eisenstein × Eisenstein),
         (∀ p ∈ P, PrimarySquarefreePair p ∧
           norm p.1 ≤ Y^(1/3+θ/16) ∧ norm p.2 ≤ Y^(1/3+θ/16)) →
         ∀ v : Eisenstein → ℂ, (∑ b ∈ B, ‖v b‖^2) ≤ E*Y^(1-θ) →
         (∑ p ∈ P, ‖∑ b ∈ B, v b*mixedCubic p.1 p.2 b‖^2) ≤
           C*Y^(7/3-θ/2)*E := by
   …

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

3. theorem OAI.CubicFirstMoment.primePower_balanced_second_moment line 116

   Source documentation

   The actual sparse higher-prime-power support satisfies the balanced second-moment saving, even when the underlying prime is small.

   theorem primePower_balanced_second_moment (hHuxley : HuxleyAdditiveLargeSieve)
       (k : ℕ) {c : ℝ} (hc : 0 < c) (hc₁ : c ≤ 1) :
       ∃ C : ℝ, 0 < C ∧ ∀ (Y A : ℝ), 1 ≤ Y → 0 ≤ A →
         ∀ B : Finset Eisenstein,
         (∀ b ∈ B, primary b ∧ (idealExponentOf b).support.card ≤ k) →
         B ⊆ largePrimePowerSupport Y c →
         ∀ P : Finset (Eisenstein × Eisenstein),
         (∀ p ∈ P, PrimarySquarefreePair p ∧
           norm p.1 ≤ Y^(1/3+c/128) ∧ norm p.2 ≤ Y^(1/3+c/128)) →
         ∀ v : Eisenstein → ℂ, (∀ b ∈ B, ‖v b‖ ≤ A) →
         (∑ p ∈ P, ‖∑ b ∈ B, v b*mixedCubic p.1 p.2 b‖^2) ≤
           C*A^2*Y^(7/3-c/16) := by
   …

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