OAI/NumberTheory/DirichletL/Inversion/FirstPriorityParents.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.SevenEighths.InverseFirstPriorityParents.Source line 15
  2. def OAI.SevenEighths.InverseFirstPriorityParents.extractedSupport line 24
  3. def OAI.SevenEighths.InverseFirstPriorityParents.parent line 29
  4. theorem OAI.SevenEighths.InverseFirstPriorityParents.parent_injective line 36
  5. def OAI.SevenEighths.InverseFirstPriorityParents.appendParent line 46
  6. def OAI.SevenEighths.InverseFirstPriorityParents.forgetAppended line 54
  7. theorem OAI.SevenEighths.InverseFirstPriorityParents.forget_append line 62
  8. theorem OAI.SevenEighths.InverseFirstPriorityParents.appendParent_injective line 69
  9. def OAI.SevenEighths.InverseFirstPriorityParents.attach line 79
  10. theorem OAI.SevenEighths.InverseFirstPriorityParents.attach_injective line 84
  11. theorem OAI.SevenEighths.InverseFirstPriorityParents.forget_attach line 98
  12. def OAI.SevenEighths.InverseFirstPriorityParents.assignmentSource line 102
  13. def OAI.SevenEighths.InverseFirstPriorityParents.assignedParents line 108
  14. theorem OAI.SevenEighths.InverseFirstPriorityParents.sum_assignmentSource line 112
  15. theorem OAI.SevenEighths.InverseFirstPriorityParents.sum_assignedParents line 125
  16. def OAI.SevenEighths.InverseFirstPriorityParents.coefficient line 134
  17. theorem OAI.SevenEighths.InverseFirstPriorityParents.coefficient_attach line 139
  18. theorem OAI.SevenEighths.InverseFirstPriorityParents.paired_parent_sum line 145
  19. theorem OAI.SevenEighths.InverseFirstPriorityParents.paired_parent_sq_sum line 158
  20. lemma OAI.SevenEighths.InverseFirstPriorityParents.mem_assignmentSource line 167
  21. theorem OAI.SevenEighths.InverseFirstPriorityParents.mem_assignedParents line 177
  22. structure OAI.SevenEighths.InverseFirstPriorityParents.SourceValid line 190
  23. theorem OAI.SevenEighths.InverseFirstPriorityParents.extracted_prime_dvd line 197
  24. theorem OAI.SevenEighths.InverseFirstPriorityParents.attach_old_support line 211
  25. theorem OAI.SevenEighths.InverseFirstPriorityParents.attach_physical_data line 232
  26. theorem OAI.SevenEighths.InverseFirstPriorityParents.coefficient_norm line 239
  27. theorem OAI.SevenEighths.InverseFirstPriorityParents.assigned_family_conditions line 250
  28. def OAI.SevenEighths.InverseFirstPriorityParents.fixedPoint line 274
  29. def OAI.SevenEighths.InverseFirstPriorityParents.fixedSource line 278
  30. theorem OAI.SevenEighths.InverseFirstPriorityParents.fixedPoint_injective line 283
  31. def OAI.SevenEighths.InverseFirstPriorityParents.parentFunction line 288
  32. theorem OAI.SevenEighths.InverseFirstPriorityParents.parentFunction_parent line 291
  33. theorem OAI.SevenEighths.InverseFirstPriorityParents.paired_source_sq_sum line 295
  34. theorem OAI.SevenEighths.InverseFirstPriorityParents.fixed_priority_complex line 304
  35. theorem OAI.SevenEighths.InverseFirstPriorityParents.fixed_priority_slice line 318
  36. def OAI.SevenEighths.InverseFirstPriorityParents.priorityOuter line 336
  37. def OAI.SevenEighths.InverseFirstPriorityParents.priorityPoisson line 343
  38. theorem OAI.SevenEighths.InverseFirstPriorityParents.first_priority_physical_slice line 356
  39. theorem OAI.SevenEighths.InverseFirstPriorityParents.first_priority_energy_reindex line 381