OAI/NumberTheory/Ostmann/Arithmetic/MovingMaskedEnergyIntegral.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The masked energy with its exact integer and harmonic-prime scales

  1. theorem OAI.Ostmann.masked_energy_fubini line 11

    Also declared: OAI/NumberTheory/Ostmann/Arithmetic/MovingSymmetrizedMaskedIntegral.lean:11 (same declaration text).

  2. theorem OAI.Ostmann.movingMaskedTemplateEnergy_interval line 40