OAI/NumberTheory/DirichletL/Moments/FirstAllocationGaussEnergy.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.CenteredMomentFirstAllocationGaussEnergy.commonEnergy line 20
  2. def OAI.SevenEighths.CenteredMomentFirstAllocationGaussEnergy.allocatedEnergy line 25
  3. lemma OAI.SevenEighths.CenteredMomentFirstAllocationGaussEnergy.common_summable line 31
  4. lemma OAI.SevenEighths.CenteredMomentFirstAllocationGaussEnergy.allocated_hasSum line 39
  5. lemma OAI.SevenEighths.CenteredMomentFirstAllocationGaussEnergy.allocated_nonneg line 49
  6. theorem OAI.SevenEighths.CenteredMomentFirstAllocationGaussEnergy.common_energy_allocation line 57
  7. def OAI.SevenEighths.CenteredMomentFirstAllocationGaussEnergy.rawVolume line 100
  8. lemma OAI.SevenEighths.CenteredMomentFirstAllocationGaussEnergy.rawVolume_pos line 103
  9. lemma OAI.SevenEighths.CenteredMomentFirstAllocationGaussEnergy.allocated_rawVolume_mul line 109
  10. lemma OAI.SevenEighths.CenteredMomentFirstAllocationGaussEnergy.allocated_rawVolume line 118
  11. lemma OAI.SevenEighths.CenteredMomentFirstAllocationGaussEnergy.rawVolume_both line 126
  12. def OAI.SevenEighths.CenteredMomentFirstAllocationGaussEnergy.frozenControl line 132
  13. lemma OAI.SevenEighths.CenteredMomentFirstAllocationGaussEnergy.frozenControl_nonneg line 135
  14. lemma OAI.SevenEighths.CenteredMomentFirstAllocationGaussEnergy.frozen_norm_bound line 139
  15. theorem OAI.SevenEighths.CenteredMomentFirstAllocationGaussEnergy.frozen_normalized_bound line 153
  16. theorem OAI.SevenEighths.CenteredMomentFirstAllocationGaussEnergy.normalized_common_energy_allocation line 183
  17. theorem OAI.SevenEighths.CenteredMomentFirstAllocationGaussEnergy.normalized_common_energy_bound line 207
  18. theorem OAI.SevenEighths.CenteredMomentFirstAllocationGaussEnergy.normalized_common_as_tsum line 241
  19. theorem OAI.SevenEighths.CenteredMomentFirstAllocationGaussEnergy.allocated_sum_hasSum line 255
  20. theorem OAI.SevenEighths.CenteredMomentFirstAllocationGaussEnergy.original_radial_bound line 266