OAI/NumberTheory/Ostmann/Arithmetic/MovingTemplateMatchedBound.lean
1 declarations, 0 contain sorry, 0 declared as axioms
The actual masked energy is bounded by its original signed pattern means
- theorem
OAI.Ostmann.movingTemplateMatchedCorrelation_pattern_boundline 11