DilatedNoncubeMass.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Actual finite noncube character mass in the enlarged conductor region used by dispersion, with the fixed coefficient-support dilation absorbed into the constants. The small enlargement is derived from the sieve gap.

lemma OAI.CubicFirstMoment.sieve_epsilon_loss line 15
Distinct definitions of this name: OAI/NumberTheory/CubicMoment/Estimates/EnlargedNoncubeMass.lean:13 (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 28
Also declared: OAI/NumberTheory/CubicMoment/Estimates/EnlargedNoncubeMass.lean:26 (same declaration text), OAI/NumberTheory/CubicMoment/Estimates/QuantitativeNoncube.lean:31 (same declaration text).
lemma OAI.CubicFirstMoment.qSieveRatio_cancel line 34
Also declared: OAI/NumberTheory/CubicMoment/Estimates/EnlargedNoncubeMass.lean:32 (same declaration text), OAI/NumberTheory/CubicMoment/Estimates/QuantitativeNoncube.lean:37 (same declaration text).
lemma OAI.CubicFirstMoment.ordinarySieveRatio_cancel line 40
Also declared: OAI/NumberTheory/CubicMoment/Estimates/EnlargedNoncubeMass.lean:38 (same declaration text), OAI/NumberTheory/CubicMoment/Estimates/QuantitativeNoncube.lean:43 (same declaration text).
lemma OAI.CubicFirstMoment.scale_sieve_row line 46
Also declared: OAI/NumberTheory/CubicMoment/Estimates/EnlargedNoncubeMass.lean:44 (same declaration text), OAI/NumberTheory/CubicMoment/Estimates/QuantitativeNoncube.lean:49 (same declaration text).

theorem OAI.CubicFirstMoment.quantitative_dilated_noncube_mass line 60

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_dilated_noncube_mass (hHuxley : HuxleyAdditiveLargeSieve)
    {K : ℝ} (hK : 1 ≤ K)
    {κ δ : ℝ} (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 ≤ K*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 → ℂ,
…

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