EnlargedNoncubeMass.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Actual finite noncube character mass in the enlarged conductor region used by dispersion. The small enlargement is derived from the sieve gap.

lemma OAI.CubicFirstMoment.sieve_epsilon_loss line 13
Distinct definitions of this name: OAI/NumberTheory/CubicMoment/Estimates/DilatedNoncubeMass.lean:15 (same declaration text), OAI/NumberTheory/CubicMoment/Estimates/QuantitativeNoncube.lean:18 (different declaration text). Qualify references as OAI.CubicFirstMoment.sieve_epsilon_loss@path.
lemma OAI.CubicFirstMoment.pSieveRatio_cancel line 26
Also declared: OAI/NumberTheory/CubicMoment/Estimates/DilatedNoncubeMass.lean:28 (same declaration text), OAI/NumberTheory/CubicMoment/Estimates/QuantitativeNoncube.lean:31 (same declaration text).
lemma OAI.CubicFirstMoment.qSieveRatio_cancel line 32
Also declared: OAI/NumberTheory/CubicMoment/Estimates/DilatedNoncubeMass.lean:34 (same declaration text), OAI/NumberTheory/CubicMoment/Estimates/QuantitativeNoncube.lean:37 (same declaration text).
lemma OAI.CubicFirstMoment.ordinarySieveRatio_cancel line 38
Also declared: OAI/NumberTheory/CubicMoment/Estimates/DilatedNoncubeMass.lean:40 (same declaration text), OAI/NumberTheory/CubicMoment/Estimates/QuantitativeNoncube.lean:43 (same declaration text).
lemma OAI.CubicFirstMoment.scale_sieve_row line 44
Also declared: OAI/NumberTheory/CubicMoment/Estimates/DilatedNoncubeMass.lean:46 (same declaration text), OAI/NumberTheory/CubicMoment/Estimates/QuantitativeNoncube.lean:49 (same declaration text).

theorem OAI.CubicFirstMoment.quantitative_enlarged_noncube_mass line 58

Source documentation

Away from the two exceptional shapes, the actual quadratic character mass saves a uniform power over B*(P*Q²)^(1/3) times coefficient energy.

theorem quantitative_enlarged_noncube_mass (hHuxley : HuxleyAdditiveLargeSieve)
    {κ δ : ℝ} (hκ : 0 < κ) (hδ : 0 < δ) :
    ∃ η C γ : ℝ, 0 < η ∧ η ≤ 1 ∧ 0 < C ∧ 0 < γ ∧
      ∀ (B p q : ℝ), 1 ≤ B → 0 ≤ p → 0 ≤ q → p+2*q ≤ 1+η →
        κ ≤ p+2*q → δ ≤ |p-1|+|q| → δ ≤ |p-1/3|+|q-1/3| →
      ∀ (A R S T J H : Finset Eisenstein),
        (∀ a ∈ A, primary a ∧ Squarefree a ∧ norm a ≤ B) →
        (∀ s ∈ S, primary s ∧ Squarefree s ∧ norm s ≤ B^p) →
        (∀ t ∈ T, primary t ∧ Squarefree t ∧ norm t ≤ B^q) →
        H ⊆ coprimeResidualSupport R J (coprimePairs S T) →
      ∀ β : Eisenstein → ℂ,
      (∑ h ∈ H, ‖∑ a ∈ A, β a*cubicSymbol a h‖^2) ≤
…

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