OAI/NumberTheory/DirichletL/Energy/FirstPhysicalNormalization.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SevenEighths.CenteredMomentEnergyFirstPhysicalNormalization.window_pair_le line 14
  2. theorem OAI.SevenEighths.CenteredMomentEnergyFirstPhysicalNormalization.pairedBudget_le_cap line 30
  3. theorem OAI.SevenEighths.CenteredMomentEnergyFirstPhysicalNormalization.pairedBudget_le_powers line 44
  4. theorem OAI.SevenEighths.CenteredMomentEnergyFirstPhysicalNormalization.physical_power_identity line 60
  5. lemma OAI.SevenEighths.CenteredMomentEnergyFirstPhysicalNormalization.character_power_identity line 71
  6. lemma OAI.SevenEighths.CenteredMomentEnergyFirstPhysicalNormalization.heightEnvelope_le line 79
  7. lemma OAI.SevenEighths.CenteredMomentEnergyFirstPhysicalNormalization.heightEnvelope_pow_le line 84
  8. def OAI.SevenEighths.CenteredMomentEnergyFirstPhysicalNormalization.normalizationConstant line 89
  9. lemma OAI.SevenEighths.CenteredMomentEnergyFirstPhysicalNormalization.normalizationConstant_pos line 92
  10. theorem OAI.SevenEighths.CenteredMomentEnergyFirstPhysicalNormalization.sourceFactor_pairedBudget_le line 101
  11. def OAI.SevenEighths.CenteredMomentEnergyFirstPhysicalNormalization.polynomialConstant line 146
  12. lemma OAI.SevenEighths.CenteredMomentEnergyFirstPhysicalNormalization.polynomialConstant_pos line 149
  13. theorem OAI.SevenEighths.CenteredMomentEnergyFirstPhysicalNormalization.sourceFactor_pairedBudget_polynomial line 154
  14. theorem OAI.SevenEighths.CenteredMomentEnergyFirstPhysicalNormalization.uniform_source_normalization line 183
  15. theorem OAI.SevenEighths.CenteredMomentEnergyFirstPhysicalNormalization.actual_physical_mass_of_columnBounds line 208