NoncubeOrdinaryBounds.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The ordinary-sieve orientation on actual ramified/cube frequency blocks.

def OAI.CubicFirstMoment.coprimeResidualSupport line 12
lemma OAI.CubicFirstMoment.residual_mixedCubic_identity line 16

theorem OAI.CubicFirstMoment.coprimeResidual_ordinary_sieve line 27

Source documentation

Huxley's inequality controls the third noncube orientation. The ramified and cube variables contribute only their explicit finite cardinalities.

theorem coprimeResidual_ordinary_sieve (hHuxley : HuxleyAdditiveLargeSieve)
    {ε : ℝ} (hε : 0 < ε) :
    ∃ C : ℝ, 0 < C ∧ ∀ (B R J : Finset Eisenstein)
      (P : Finset (Eisenstein × Eisenstein)) (Q Z : ℝ), 1 ≤ Q → 1 ≤ Z →
      (∀ p ∈ P, PrimarySquarefreePair p ∧ norm (pairConductor p) ≤ Q) →
      (∀ b ∈ B, primary b ∧ norm b ≤ Z) → ∀ v : Eisenstein → ℂ,
      (∑ h ∈ coprimeResidualSupport R J P, ‖∑ b ∈ B, v b*cubicSymbol b h‖^2) ≤
        (R.card:ℝ)*J.card*C*Q^ε*(Q^2+Z)*∑ b ∈ B, ‖v b‖^2 := by
…

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