OAI/NumberTheory/Ostmann/Arithmetic/MovingPatternBadEventRate.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Collision and deletion errors for the actual pattern kernel

  1. theorem OAI.Ostmann.movingPattern_bad_event_rate line 13
  2. theorem OAI.Ostmann.movingPattern_bad_event_rate_window line 87

    Source documentation

    Collision and deletion errors uniformly over the moving Fourier window.

    theorem movingPattern_bad_event_rate_window (ฯˆ : ๐“ข(โ„, โ„‚)) (n rโ‚€ k : โ„•)
    (A H B D F Cnorm : โ„) (hA : 0 โ‰ค A) (hH : 0 โ‰ค H) (hF : 0 โ‰ค F) :
    โˆ€แถ  L : โ„ in atTop, let m := spectatorBulkCount k L
โ€ฆ

    Mentions: OAI.Ostmann.spectatorBulkCount