OAI/NumberTheory/DirichletL/Moments/AllocatedNaturalRadial.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SevenEighths.CenteredMomentAllocatedNaturalRadial.profile_support line 20
  2. def OAI.SevenEighths.CenteredMomentAllocatedNaturalRadial.naturalCharacter line 29
  3. lemma OAI.SevenEighths.CenteredMomentAllocatedNaturalRadial.naturalCharacter_eq line 32
  4. def OAI.SevenEighths.CenteredMomentAllocatedNaturalRadial.Shared line 37
  5. theorem OAI.SevenEighths.CenteredMomentAllocatedNaturalRadial.uniform_shared line 59
  6. def OAI.SevenEighths.CenteredMomentAllocatedNaturalRadial.commonChild line 79
  7. lemma OAI.SevenEighths.CenteredMomentAllocatedNaturalRadial.common_rawScale line 90
  8. theorem OAI.SevenEighths.CenteredMomentAllocatedNaturalRadial.common_allocated_normalized line 97
  9. theorem OAI.SevenEighths.CenteredMomentAllocatedNaturalRadial.allocated_radial_bound line 122
  10. theorem OAI.SevenEighths.CenteredMomentAllocatedNaturalRadial.natural_child_summable line 165
  11. lemma OAI.SevenEighths.CenteredMomentAllocatedNaturalRadial.common_nonzero line 192
  12. lemma OAI.SevenEighths.CenteredMomentAllocatedNaturalRadial.child_energy_eq_radial line 196
  13. def OAI.SevenEighths.CenteredMomentAllocatedNaturalRadial.CommonBound line 216
  14. theorem OAI.SevenEighths.CenteredMomentAllocatedNaturalRadial.actual_common_radial_energy line 231
  15. lemma OAI.SevenEighths.CenteredMomentAllocatedNaturalRadial.nonexceptional_nonzero line 257
  16. theorem OAI.SevenEighths.CenteredMomentAllocatedNaturalRadial.uniform_initial_common_radial_energy line 261
  17. lemma OAI.SevenEighths.CenteredMomentAllocatedNaturalRadial.common_raw_same_product line 277
  18. theorem OAI.SevenEighths.CenteredMomentAllocatedNaturalRadial.original_nonexceptional_common_radial_energy line 284