OAI/NumberTheory/Ostmann/Arithmetic/MovingTemplateEnergyPatterns.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.movingTemplateDiagonalEnergy_pattern_boundline 11