OAI/NumberTheory/Ostmann/Arithmetic/MovingPatternInternalError.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The internal-prime error for the literal moving pattern cost

  1. theorem OAI.Ostmann.movingPattern_internal_arithmetic_error_rate line 14

    Source documentation

    All internal class counts and moving windows share the same eventual error bound. Only the original point-mass bounds on the priors are used.

    theorem movingPattern_internal_arithmetic_error_rate (ฯˆ : ๐“ข(โ„, โ„‚)) (n rโ‚€ k : โ„•)
    (A Wwin B D E : โ„) (hA : 0 โ‰ค A) (hWwin : 0 โ‰ค Wwin) (hE : 0 โ‰ค E) :
    โˆ€แถ  L : โ„ in atTop, let m := spectatorBulkCount k L
โ€ฆ

    Mentions: OAI.Ostmann.spectatorBulkCount