OAI/NumberTheory/Ostmann/Arithmetic/MovingPatternPrimeNorm.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Pointwise bound for the literal original prime observable

  1. theorem OAI.Ostmann.movingPatternPrimeBulkHaar_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 movingPatternPrimeBulkHaar_norm
    (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