RegularWeightCap.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Polynomial caps supplied by the total-count regularity condition

theorem OAI.JointDickman.regular_scale_cap line 12

theorem OAI.JointDickman.regular_weights_cap line 50

Source documentation

Equation (8), with an arbitrary positive exponent slack replacing o(1). The bound is uniform in the tail tolerance C and in the selected prime set.

theorem regular_weights_cap {L : ℕ} (hL : 1 ≤ L) {τ ε : ℝ}
    (hτ : 0 ≤ τ) (hε : 0 < ε) :
    ∀ᶠ B : ℕ in atTop, ∀ C : ℝ,
      (∀ S : Finset ℕ, regularResidueWeight B L τ C S ≤ (B : ℝ) ^ (weightExponent τ + ε)) ∧
      (∀ n : ℕ, regularCoefficientWeight B L τ C n ≤ (B : ℝ) ^ (weightExponent τ + ε)) := by
…

Mentions: OAI.JointDickman.regularResidueWeight, OAI.JointDickman.weightExponent, OAI.JointDickman.regularCoefficientWeight