OAI/NumberTheory/DirichletL/Inversion/WholePriorityRetainedSource.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.InverseWholePriorityRetainedSource.unifiedSource line 17
  2. theorem OAI.SevenEighths.InverseWholePriorityRetainedSource.mem_unifiedSource line 24
  3. theorem OAI.SevenEighths.InverseWholePriorityRetainedSource.unified_frequency_ne_zero line 34
  4. theorem OAI.SevenEighths.InverseWholePriorityRetainedSource.unified_mem_sector line 41
  5. theorem OAI.SevenEighths.InverseWholePriorityRetainedSource.sectors_sum line 54
  6. theorem OAI.SevenEighths.InverseWholePriorityRetainedSource.parent_retained_sum line 73
  7. theorem OAI.SevenEighths.InverseWholePriorityRetainedSource.unified_conditions line 88
  8. theorem OAI.SevenEighths.InverseWholePriorityRetainedSource.unified_deleted_support line 99
  9. theorem OAI.SevenEighths.InverseWholePriorityRetainedSource.deleted_lists line 116
  10. def OAI.SevenEighths.InverseWholePriorityRetainedSource.wholeRow line 125
  11. theorem OAI.SevenEighths.InverseWholePriorityRetainedSource.wholeRow_eq line 133
  12. theorem OAI.SevenEighths.InverseWholePriorityRetainedSource.whole_retained_sum line 150
  13. def OAI.SevenEighths.InverseWholePriorityRetainedSource.activeParents line 189
  14. theorem OAI.SevenEighths.InverseWholePriorityRetainedSource.active_conditions line 195
  15. theorem OAI.SevenEighths.InverseWholePriorityRetainedSource.active_deleted_support line 208
  16. def OAI.SevenEighths.InverseWholePriorityRetainedSource.coefficientBound line 225
  17. theorem OAI.SevenEighths.InverseWholePriorityRetainedSource.coefficientBound_pos line 227
  18. theorem OAI.SevenEighths.InverseWholePriorityRetainedSource.priorityOuter_norm line 231
  19. def OAI.SevenEighths.InverseWholePriorityRetainedSource.sourceWeight line 250
  20. theorem OAI.SevenEighths.InverseWholePriorityRetainedSource.sourceWeight_norm line 256
  21. def OAI.SevenEighths.InverseWholePriorityRetainedSource.normalizedWeight line 277
  22. theorem OAI.SevenEighths.InverseWholePriorityRetainedSource.normalizedWeight_norm line 282
  23. theorem OAI.SevenEighths.InverseWholePriorityRetainedSource.source_sum_normalized line 303
  24. theorem OAI.SevenEighths.InverseWholePriorityRetainedSource.fullPhysical_unified line 317
  25. theorem OAI.SevenEighths.InverseWholePriorityRetainedSource.actual_retained_normalized line 344