NumericAdditionClass.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Summing a class of actual numeric additions

A class fixes the retained coefficient, the opposite coefficient, the lag, the number of added primes, and a factor-four product window. The alternative quotient remains regular. Its weighted sum is reduced to one progression.

theorem OAI.JointDickman.primePrefix_exponent_mono line 18
def OAI.JointDickman.numericAdditionClass line 32
theorem OAI.JointDickman.mem_numericAdditionClass line 39
def OAI.JointDickman.additionProgressionWeight line 47
theorem OAI.JointDickman.additionProgressionWeight_nonneg line 53

theorem OAI.JointDickman.numeric_addition_class_progression_bound line 62

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 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 = b+j*c →
      z = z₀+j*(z/j) ∧ (c : ℤ) = c₀+(e : ℤ)*((z/j : ℕ) : ℤ)) :
    (∑ Z ∈ numericAdditionClass 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),
          additionProgressionWeight B g e j b z₀ c₀ q n := by
…

Mentions: OAI.JointDickman.numericAdditionClass, OAI.JointDickman.auxiliaryLogLength, OAI.JointDickman.additionIntervalLower, OAI.JointDickman.additionIntervalUpper, OAI.JointDickman.additionProgressionWeight