SparseFourthMoment.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The square of a structured error polynomial has controlled coefficient energy. This supplies the fourth-moment estimate in the balanced range.

def OAI.CubicFirstMoment.productSupport line 14
def OAI.CubicFirstMoment.squareConvolution line 17
lemma OAI.CubicFirstMoment.second_moment_sq_le_card_fourth line 20

lemma OAI.CubicFirstMoment.primeProduct_pair_fiber_card line 27

Source documentation

Every pair of products of k supported primes is the image of a 2k-prime tuple. Thus the multiplicity costs a constant depending on k.

lemma primeProduct_pair_fiber_card {ι : Type*} [Fintype ι] [DecidableEq ι]
    (S : ι → Finset Eisenstein) (hS : ∀ i, ∀ p ∈ S i, primaryPrime p)
    (n : Eisenstein) :
    (((orderedConvolutionSupport S).product (orderedConvolutionSupport S)).filter
      (fun z => z.1*z.2 = n)).card ≤
        (2*Fintype.card ι)^(2*Fintype.card ι) := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primaryPrime, OAI.CubicFirstMoment.orderedConvolutionSupport

lemma OAI.CubicFirstMoment.squareConvolution_character line 61
lemma OAI.CubicFirstMoment.squareConvolution_energy line 87

theorem OAI.CubicFirstMoment.ordinary_mixed_fourth_moment line 117

Source documentation

Apply the ordinary character sieve to the actual squared polynomial. The input multiplicity is purely arithmetic and is discharged below for bounded-length products of primes.

theorem ordinary_mixed_fourth_moment (hHuxley : HuxleyAdditiveLargeSieve)
    {ε : ℝ} (hε : 0 < ε) :
    ∃ C : ℝ, 0 < C ∧ ∀ (Q Z : ℝ), 1 ≤ Q → 1 ≤ Z →
      ∀ (P : Finset (Eisenstein × Eisenstein)) (B : Finset Eisenstein),
      (∀ p ∈ P, PrimarySquarefreePair p ∧ norm (pairConductor p) ≤ Q) →
      (∀ b ∈ B, b ≠ 0 ∧ norm b ≤ Z) →
      ∀ (K : ℝ), (∀ n ∈ productSupport B,
        (((B.product B).filter (fun z => z.1*z.2 = n)).card:ℝ) ≤ K) →
      ∀ v : Eisenstein → ℂ,
      (∑ p ∈ P, ‖∑ b ∈ B, v b*mixedCubic p.1 p.2 b‖^4) ≤
        C*Q^ε*(Q^2+Z^2)*K*(∑ b ∈ B, ‖v b‖^2)^2 := by
…

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

theorem OAI.CubicFirstMoment.primeProduct_mixed_fourth_moment line 153

theorem OAI.CubicFirstMoment.primeConvolutionError_twisted_fourth_moment line 180

Source documentation

The actual repeated-prime error saves a power in the fourth moment, uniformly under fixed angular and arbitrary real norm twists.

theorem primeConvolutionError_twisted_fourth_moment
    {ι : Type*} [Fintype ι] [DecidableEq ι]
    (hHuxley : HuxleyAdditiveLargeSieve) {ε : ℝ} (hε : 0 < ε) :
    ∃ C : ℝ, 0 < C ∧ ∀ (S : ι → Finset Eisenstein)
      (w : ι → Eisenstein → ℂ) (M : ι → ℝ) (Y c Q : ℝ),
      1 ≤ Y → 1 ≤ Q → (∀ i, 0 ≤ M i) →
      (∀ i, ∀ p ∈ S i, primaryPrime p ∧ Y^c < norm p) →
      (∀ f ∈ Fintype.piFinset S, norm (∏ i, f i) ≤ Y) →
      (∀ i, ∀ p ∈ S i, ‖w i p‖ ≤ M i) →
      ∀ P : Finset (Eisenstein × Eisenstein),
      (∀ p ∈ P, PrimarySquarefreePair p ∧ norm (pairConductor p) ≤ Q) →
      ∀ (ℓ : ℤ) (u : ℝ) (ν : Eisenstein → ℂ),
…

Mentions: OAI.CubicFirstMoment.HuxleyAdditiveLargeSieve, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primaryPrime, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.PrimarySquarefreePair, OAI.CubicFirstMoment.pairConductor