NoncubeSieveAssembly.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

All three sieve orientations on the same concrete noncube frequency block.

def OAI.CubicFirstMoment.coprimePairs line 13
lemma OAI.CubicFirstMoment.coprimeResidualSupport_subset line 16

theorem OAI.CubicFirstMoment.noncube_three_sieve_bounds line 31

Source documentation

The two cubic estimates and the ordinary estimate apply to the same positive mass; no exceptional-moment hypothesis is used.

theorem noncube_three_sieve_bounds (hHuxley : HuxleyAdditiveLargeSieve)
    {ε : ℝ} (hε : 0 < ε) :
    ∃ C₁ C₂ : ℝ, 0 < C₁ ∧ 0 < C₂ ∧
    ∀ (B R S T J H : Finset Eisenstein) (N U V : ℝ),
      1 ≤ N → 1 ≤ U → 1 ≤ V →
      (∀ b ∈ B, primary b ∧ Squarefree b ∧ norm b ≤ N) →
      (∀ s ∈ S, primary s ∧ Squarefree s ∧ norm s ≤ U) →
      (∀ t ∈ T, primary t ∧ Squarefree t ∧ norm t ≤ V) →
      H ⊆ coprimeResidualSupport R J (coprimePairs S T) →
      ∀ β : Eisenstein → ℂ,
      (∑ h ∈ H, ‖∑ b ∈ B, β b*cubicSymbol b h‖^2) ≤
        min ((R.card:ℝ)*J.card*C₁ *
…

Mentions: OAI.CubicFirstMoment.HuxleyAdditiveLargeSieve, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.coprimeResidualSupport, OAI.CubicFirstMoment.coprimePairs, OAI.CubicFirstMoment.cubicSymbol