OAI/NumberTheory/DirichletL/Moments/AmplificationChildInput.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.CenteredMomentAmplificationChildInput.original line 24
  2. def OAI.SevenEighths.CenteredMomentAmplificationChildInput.volume line 40
  3. theorem OAI.SevenEighths.CenteredMomentAmplificationChildInput.volume_pos line 42
  4. theorem OAI.SevenEighths.CenteredMomentAmplificationChildInput.residual_ne line 45
  5. theorem OAI.SevenEighths.CenteredMomentAmplificationChildInput.residual_one line 50
  6. theorem OAI.SevenEighths.CenteredMomentAmplificationChildInput.residual_coverage line 55
  7. def OAI.SevenEighths.CenteredMomentAmplificationChildInput.child line 63
  8. theorem OAI.SevenEighths.CenteredMomentAmplificationChildInput.child_modulus line 80
  9. theorem OAI.SevenEighths.CenteredMomentAmplificationChildInput.child_character line 83
  10. theorem OAI.SevenEighths.CenteredMomentAmplificationChildInput.child_height line 86
  11. theorem OAI.SevenEighths.CenteredMomentAmplificationChildInput.live_slot_one line 89
  12. theorem OAI.SevenEighths.CenteredMomentAmplificationChildInput.child_tuplePool line 92
  13. theorem OAI.SevenEighths.CenteredMomentAmplificationChildInput.child_profile line 110
  14. theorem OAI.SevenEighths.CenteredMomentAmplificationChildInput.prime_slot_one line 119
  15. theorem OAI.SevenEighths.CenteredMomentAmplificationChildInput.prime_slots_live line 125
  16. theorem OAI.SevenEighths.CenteredMomentAmplificationChildInput.prime_plain_norm_product line 130
  17. theorem OAI.SevenEighths.CenteredMomentAmplificationChildInput.child_products line 137
  18. theorem OAI.SevenEighths.CenteredMomentAmplificationChildInput.child_volume line 150
  19. theorem OAI.SevenEighths.CenteredMomentAmplificationChildInput.child_slot_card line 160
  20. theorem OAI.SevenEighths.CenteredMomentAmplificationChildInput.child_slot_scale_ge_one line 165
  21. theorem OAI.SevenEighths.CenteredMomentAmplificationChildInput.child_plain_annuli line 169
  22. theorem OAI.SevenEighths.CenteredMomentAmplificationChildInput.child_columns line 176
  23. theorem OAI.SevenEighths.CenteredMomentAmplificationChildInput.child_gauss_source line 195
  24. def OAI.SevenEighths.CenteredMomentAmplificationChildInput.normalizedGaussSource line 210
  25. def OAI.SevenEighths.CenteredMomentAmplificationChildInput.childNormalizedGaussSource line 214
  26. theorem OAI.SevenEighths.CenteredMomentAmplificationChildInput.original_childEnergy_eq_inputs line 218