OAI/NumberTheory/JointDickman/Amplification/PrefixViolationSum.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Summing the actual prefix failures on a fixed grid

  1. def OAI.JointDickman.prefixGridError line 12
  2. theorem OAI.JointDickman.prefixGridError_nonneg line 17
  3. theorem OAI.JointDickman.prefixGridError_tendsto line 23
  4. theorem OAI.JointDickman.sum_le_linear_remainder line 45

    Source documentation

    Finite summation of a common main factor and uniformly bounded remainders.

    theorem sum_le_linear_remainder {ι : Type*} (S : Finset ι)
    (f t r : ι → ℝ) {A E R : ℝ} (hE : 0 ≤ E)
    (hf : ∀ i ∈ S, f i ≤ A * t i + r i * E)
    (hr : ∀ i ∈ S, r i ≤ R) :
    (∑ i ∈ S, f i) ≤ A * (∑ i ∈ S, t i) + (S.card : ℝ) * R * E := by
…
  5. theorem OAI.JointDickman.coefficient_prefix_sum_bound line 55