OAI/NumberTheory/CubicMoment/Estimates/SparseModelCounting.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CubicFirstMoment.squarefree_model_bilinear_counting line 11
2. lemma OAI.CubicFirstMoment.sparse_model_counting_scale line 77
3. lemma OAI.CubicFirstMoment.squarefree_model_bilinear_operator line 101

   Source documentation

   The squarefree model has at most the cubic-sieve shape by direct finite counting. No cancellation or model asymptotic is assumed.

   lemma squarefree_model_bilinear_operator
       (P Q : Finset Eisenstein) (α β : Eisenstein → ℂ) (V : Eisenstein → Eisenstein → ℂ)
       {A B M H ε : ℝ} (hA : 1 ≤ A) (hB : 1 ≤ B) (hM : 0 < M)
       (hH : 0 ≤ H) (hε : 0 ≤ ε)
       (hP : ∀ a ∈ P, primary a ∧ A/M ≤ norm a ∧ norm a ≤ A)
       (hQ : ∀ b ∈ Q, primary b ∧ B/M ≤ norm b ∧ norm b ≤ B)
       (hV : ∀ a ∈ P, ∀ b ∈ Q, ‖V a b‖ ≤ H) :
       ‖∑ a ∈ P, ∑ b ∈ Q, α a*β b*(idealMoebius (a*b):ℂ)^2*
         ((norm (a*b)^(-1/6:ℝ):ℝ):ℂ)*V a b‖^2 ≤
         (324*H^2*M^(2/3:ℝ))*(A*B)^ε*(A+B+(A*B)^(2/3:ℝ))*
           (∑ a ∈ P, ‖α a‖^2)*(∑ b ∈ Q, ‖β b‖^2) := by
   …

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