OAI/NumberTheory/JointDickman/Counting/EnergyMeanComparison.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Passing from periodic mean-square energy to mean energy

  1. theorem OAI.JointDickman.complexEnergy_sub line 10
  2. theorem OAI.JointDickman.normalized_energy_comparison line 15
  3. theorem OAI.JointDickman.finite_norm_mean_of_square line 29