OAI/NumberTheory/JointDickman/Amplification/LowNumericAdditionClass.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.lowNumericAdditionClass line 12
2. theorem OAI.JointDickman.mem_lowNumericAdditionClass line 19
3. theorem OAI.JointDickman.low_numeric_addition_class_progression_bound line 30

   Source documentation

   The progression parametrization is injective on the squarefree prime products in a class. The remaining quotient's regularity supplies exactly one half-weight factor, before the numeric interval is enlarged.

   theorem low_numeric_addition_class_progression_bound {B L k e j b d z₀ : ℕ}
       {τ C W g q : ℝ} {c₀ : ℤ}
       (hB : 1 ≤ B) (hk : k ∈ Icc 1 L) (hg : g ≤ (k : ℝ)/L)
       (hq : 0 < q) (hq1 : q ≤ 1)
       (hprogress : ∀ z c : ℕ, e*z+j*c = b →
         z = z₀+j*(z/j) ∧ (c : ℤ) = c₀-(e : ℤ)*((z/j : ℕ) : ℤ)) :
       (∑ Z ∈ lowNumericAdditionClass B L τ C e j b d W,
         (1/2 : ℝ)^d/((∏ p ∈ Z, p : ℕ) : ℝ)) ≤
         (((1/2 : ℝ)/q)^d*Real.exp (((((k : ℝ)/L)/2+τ)*auxiliaryLogLength B)*Real.log 2))*
           ∑ n ∈ Ico (additionIntervalLower W j) (additionIntervalUpper W j),
             lowAdditionProgressionWeight B g e j b z₀ c₀ q n := by
   …

   Mentions: OAI.JointDickman.lowNumericAdditionClass, OAI.JointDickman.auxiliaryLogLength, OAI.JointDickman.additionIntervalLower, OAI.JointDickman.additionIntervalUpper, OAI.JointDickman.lowAdditionProgressionWeight