OAI/NumberTheory/DirichletL/Moments/AllocatedNaturalSource.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.SevenEighths.CenteredMomentAllocatedNaturalSource.Plain line 18
  2. def OAI.SevenEighths.CenteredMomentAllocatedNaturalSource.Plain.profile line 26
  3. lemma OAI.SevenEighths.CenteredMomentAllocatedNaturalSource.Plain.profile_retained line 29
  4. lemma OAI.SevenEighths.CenteredMomentAllocatedNaturalSource.Plain.profile_zero line 33
  5. lemma OAI.SevenEighths.CenteredMomentAllocatedNaturalSource.polynomial_zero line 36
  6. theorem OAI.SevenEighths.CenteredMomentAllocatedNaturalSource.retained_normalized line 40
  7. def OAI.SevenEighths.CenteredMomentAllocatedNaturalSource.rawScale line 68
  8. lemma OAI.SevenEighths.CenteredMomentAllocatedNaturalSource.rawScale_pos line 71
  9. lemma OAI.SevenEighths.CenteredMomentAllocatedNaturalSource.raw_same_product line 76
  10. theorem OAI.SevenEighths.CenteredMomentAllocatedNaturalSource.allocated_normalized line 81
  11. theorem OAI.SevenEighths.CenteredMomentAllocatedNaturalSource.slot_controls line 107
  12. def OAI.SevenEighths.CenteredMomentAllocatedNaturalSource.SharedBound line 119
  13. theorem OAI.SevenEighths.CenteredMomentAllocatedNaturalSource.uniform_shared line 140
  14. lemma OAI.SevenEighths.CenteredMomentAllocatedNaturalSource.primeSupport_product_radical line 156
  15. def OAI.SevenEighths.CenteredMomentAllocatedNaturalSource.child line 163
  16. def OAI.SevenEighths.CenteredMomentAllocatedNaturalSource.AllocatedBound line 172
  17. theorem OAI.SevenEighths.CenteredMomentAllocatedNaturalSource.allocated_energy line 191
  18. theorem OAI.SevenEighths.CenteredMomentAllocatedNaturalSource.uniform_allocated_energy line 214
  19. theorem OAI.SevenEighths.CenteredMomentAllocatedNaturalSource.natural_nonprincipal_width line 231
  20. structure OAI.SevenEighths.CenteredMomentAllocatedNaturalSource.Slots line 242
  21. def OAI.SevenEighths.CenteredMomentAllocatedNaturalSource.Slots.coefficient line 253
  22. lemma OAI.SevenEighths.CenteredMomentAllocatedNaturalSource.Slots.controls line 257
  23. structure OAI.SevenEighths.CenteredMomentAllocatedNaturalSource.Row line 262
  24. lemma OAI.SevenEighths.CenteredMomentAllocatedNaturalSource.Row.extracted_same_product line 280
  25. theorem OAI.SevenEighths.CenteredMomentAllocatedNaturalSource.uniform_paired_nuW_energy line 285
  26. def OAI.SevenEighths.CenteredMomentAllocatedNaturalSource.inputSlots line 329
  27. lemma OAI.SevenEighths.CenteredMomentAllocatedNaturalSource.inputSlots_coefficient line 341
  28. def OAI.SevenEighths.CenteredMomentAllocatedNaturalSource.commonSlots line 344
  29. lemma OAI.SevenEighths.CenteredMomentAllocatedNaturalSource.commonSlots_coefficient line 358