UnrestrictedCubicSieve.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The proved cubic large sieve with an unrestricted inner coefficient support. The cube decomposition is already in the baseline; here its summed dyadic bound is transferred to a sharp norm cutoff.

lemma OAI.CubicFirstMoment.finiteCubicBound_le_dualDyadicNorm line 15
lemma OAI.CubicFirstMoment.inverse_negative_rpow line 68

theorem OAI.CubicFirstMoment.unrestricted_cubic_operator_bound line 74

Source documentation

Sharp cutoff form of the cube-extracted cubic sieve. The inner support need not be squarefree or primary.

theorem unrestricted_cubic_operator_bound {ε : ℝ} (hε : 0 < ε) (hε₁ : ε ≤ 1) :
    ∃ C : ℝ, 0 < C ∧ ∀ (P H : Finset Eisenstein) (N Z : ℝ),
      1 ≤ N → 1 ≤ Z →
      (∀ p ∈ P, primary p ∧ Squarefree p ∧ norm p ≤ N) →
      (∀ h ∈ H, h ≠ 0 ∧ norm h ≤ Z) →
      finiteCubicBound P H ≤ C*(N*Z)^ε*
        (N*Z^(1/3:ℝ)+(N*Z)^(2/3:ℝ)+Z^(4/3:ℝ)+Z) := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.finiteCubicBound

lemma OAI.CubicFirstMoment.finiteCubicBound_controls_transpose line 98
Source documentation
Transposition of the actual finite cubic-character matrix. This does not require reciprocity or primarity of the inner support.
```
lemma finiteCubicBound_controls_transpose (P H : Finset Eisenstein)
    (v : Eisenstein → ℂ) :
    (∑ p ∈ P, ‖∑ h ∈ H, v h*cubicSymbol p h‖^2) ≤
      finiteCubicBound P H * ∑ h ∈ H, ‖v h‖^2 := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.cubicSymbol, OAI.CubicFirstMoment.finiteCubicBound
theorem OAI.CubicFirstMoment.unrestricted_cubic_sieve line 141