OAI/NumberTheory/DirichletL/Inversion/PrioritySecondSource.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.InversePrioritySecondSource.quotientSupport line 17
  2. theorem OAI.SevenEighths.InversePrioritySecondSource.quotientSupport_parent line 20
  3. theorem OAI.SevenEighths.InversePrioritySecondSource.quotientSupport_attach line 25
  4. def OAI.SevenEighths.InversePrioritySecondSource.residualLists line 30
  5. theorem OAI.SevenEighths.InversePrioritySecondSource.residualLists_attach line 36
  6. theorem OAI.SevenEighths.InversePrioritySecondSource.residualLists_disjoint line 47
  7. theorem OAI.SevenEighths.InversePrioritySecondSource.assigned_quotient line 54
  8. def OAI.SevenEighths.InversePrioritySecondSource.retainedPool line 63
  9. theorem OAI.SevenEighths.InversePrioritySecondSource.mem_retainedPool line 71
  10. theorem OAI.SevenEighths.InversePrioritySecondSource.retainedPool_conditions line 80
  11. theorem OAI.SevenEighths.InversePrioritySecondSource.retainedPool_original_support line 93
  12. def OAI.SevenEighths.InversePrioritySecondSource.attachOriginal line 107
  13. theorem OAI.SevenEighths.InversePrioritySecondSource.attachOriginal_injective line 113
  14. theorem OAI.SevenEighths.InversePrioritySecondSource.retainedPool_iff_original line 121
  15. theorem OAI.SevenEighths.InversePrioritySecondSource.attached_coefficient line 146
  16. theorem OAI.SevenEighths.InversePrioritySecondSource.varying_lists_parent_family line 156
  17. def OAI.SevenEighths.InversePrioritySecondSource.parentPoisson line 185
  18. theorem OAI.SevenEighths.InversePrioritySecondSource.parentPoisson_attach line 196
  19. def OAI.SevenEighths.InversePrioritySecondSource.retainedRow line 209
  20. theorem OAI.SevenEighths.InversePrioritySecondSource.parentPoisson_full line 218
  21. theorem OAI.SevenEighths.InversePrioritySecondSource.retained_sum line 276
  22. theorem OAI.SevenEighths.InversePrioritySecondSource.commute_parent_sectors line 292
  23. theorem OAI.SevenEighths.InversePrioritySecondSource.parent_family_full line 305
  24. def OAI.SevenEighths.InversePrioritySecondSource.fullSource line 365
  25. theorem OAI.SevenEighths.InversePrioritySecondSource.first_priority_physical_source line 384
  26. theorem OAI.SevenEighths.InversePrioritySecondSource.fixed_retained_conditions line 436