PrimarySparseMoment.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Sparse coefficient energy in the balanced conductor region. The pair multiplicity is bounded using actual primary divisors, with no restriction on the number of prime bases.

lemma OAI.CubicFirstMoment.primary_pair_fiber_power line 14
theorem OAI.CubicFirstMoment.primary_mixed_fourth_moment line 41
lemma OAI.CubicFirstMoment.balancedPrimary_power line 57

theorem OAI.CubicFirstMoment.primary_balanced_sparse_moment line 88

Source documentation

The sparse coefficient energy and the primary divisor bound suffice for the actual balanced mixed-character second moment.

theorem primary_balanced_sparse_moment
    (hHuxley : HuxleyAdditiveLargeSieve) {θ : ℝ}
    (hθ : 0 < θ) (hθ₁ : θ ≤ 1) :
    ∃ C : ℝ, 0 < C ∧ ∀ (Y E : ℝ), 1 ≤ Y → 0 ≤ E →
      ∀ B : Finset Eisenstein,
      (∀ b ∈ B, primary b ∧ norm b ≤ Y) →
      ∀ 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.PrimarySquarefreePair, OAI.CubicFirstMoment.mixedCubic