OAI/NumberTheory/CubicMoment/Estimates/QuantitativeNoncube.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The uniform exponent saving applied to the actual finite frequency mass.

  1. lemma OAI.CubicFirstMoment.primary_support_card_le line 12
  2. lemma OAI.CubicFirstMoment.sieve_epsilon_loss line 18

    Distinct definitions of this name: OAI/NumberTheory/CubicMoment/Estimates/DilatedNoncubeMass.lean:15 (different declaration text), OAI/NumberTheory/CubicMoment/Estimates/EnlargedNoncubeMass.lean:13 (different declaration text). Qualify references as OAI.CubicFirstMoment.sieve_epsilon_loss@path.

  3. lemma OAI.CubicFirstMoment.pSieveRatio_cancel line 31

    Also declared: OAI/NumberTheory/CubicMoment/Estimates/DilatedNoncubeMass.lean:28 (same declaration text), OAI/NumberTheory/CubicMoment/Estimates/EnlargedNoncubeMass.lean:26 (same declaration text).

  4. lemma OAI.CubicFirstMoment.qSieveRatio_cancel line 37

    Also declared: OAI/NumberTheory/CubicMoment/Estimates/DilatedNoncubeMass.lean:34 (same declaration text), OAI/NumberTheory/CubicMoment/Estimates/EnlargedNoncubeMass.lean:32 (same declaration text).

  5. lemma OAI.CubicFirstMoment.ordinarySieveRatio_cancel line 43

    Also declared: OAI/NumberTheory/CubicMoment/Estimates/DilatedNoncubeMass.lean:40 (same declaration text), OAI/NumberTheory/CubicMoment/Estimates/EnlargedNoncubeMass.lean:38 (same declaration text).

  6. lemma OAI.CubicFirstMoment.scale_sieve_row line 49

    Also declared: OAI/NumberTheory/CubicMoment/Estimates/DilatedNoncubeMass.lean:46 (same declaration text), OAI/NumberTheory/CubicMoment/Estimates/EnlargedNoncubeMass.lean:44 (same declaration text).

  7. theorem OAI.CubicFirstMoment.quantitative_noncube_mass line 63

    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_noncube_mass (hHuxley : HuxleyAdditiveLargeSieve)
    {κ δ : ℝ} (hκ : 0 < κ) (hδ : 0 < δ) :
    ∃ C γ : ℝ, 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