MovingPatternTwoPrimeNorm.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Pointwise bound for the literal original prime observable

theorem OAI.Ostmann.movingPatternTwoPrimeBulkHaar_norm line 43

Source documentation

This uniform pointwise estimate allows the extra nonbulk-prime deletion error to be returned to the initial external law.

theorem movingPatternTwoPrimeBulkHaar_norm
    (hxg : 0 ≤ xg) (hy : 0 ≤ y) (Kspec : I → ℝ) (hKspec : ∀ i, 0 ≤ Kspec i)
    (hgnorm : ∀ i z, ‖g i z‖ ≤ Kspec i)
    (x : (TreeLeafIndex n × Fin m) → primes) :
    let data := movingPatternFinBulkData e n m t small slot perm pattern
…

Mentions: OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.primes, OAI.Ostmann.movingPatternFinBulkData