OAI/NumberTheory/Ostmann/Arithmetic/MovingPatternSignedSum.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Summing the signed pattern bounds without a bulk-length loss

  1. theorem OAI.Ostmann.movingPattern_signed_sum_bound line 12

    Source documentation

    The per-class comparison error and signed bulk remainder can be summed across every equality pattern with a cost depending only on the fixed depth.

    theorem movingPattern_signed_sum_bound (n : ℕ) (E D τ K : ℝ)
    (hE : 0 ≤ E) (hD : 0 ≤ D) (hτ : 0 ≤ τ) (hK : 0 ≤ K) :
    let _ := sampleSetoidFintype (Bool × MovingSampleIndex n)
…

    Mentions: OAI.Ostmann.sampleSetoidFintype, OAI.Ostmann.MovingSampleIndex