OAI/NumberTheory/DirichletL/Inversion/InitialEnergyCallerAssigned.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.InverseInitialEnergyCallerAssigned.attach line 13
  2. def OAI.SevenEighths.InverseInitialEnergyCallerAssigned.erase line 20
  3. theorem OAI.SevenEighths.InverseInitialEnergyCallerAssigned.erase_attach line 28
  4. theorem OAI.SevenEighths.InverseInitialEnergyCallerAssigned.attach_injective line 35
  5. def OAI.SevenEighths.InverseInitialEnergyCallerAssigned.attachPair line 42
  6. theorem OAI.SevenEighths.InverseInitialEnergyCallerAssigned.attachPair_injective line 48
  7. def OAI.SevenEighths.InverseInitialEnergyCallerAssigned.assignedSource line 57
  8. def OAI.SevenEighths.InverseInitialEnergyCallerAssigned.coefficient line 63
  9. theorem OAI.SevenEighths.InverseInitialEnergyCallerAssigned.coefficient_attach line 71
  10. theorem OAI.SevenEighths.InverseInitialEnergyCallerAssigned.assignedSource_sum line 77
  11. theorem OAI.SevenEighths.InverseInitialEnergyCallerAssigned.original_marks_eq_assigned line 90
  12. theorem OAI.SevenEighths.InverseInitialEnergyCallerAssigned.assignedSource_support line 107
  13. theorem OAI.SevenEighths.InverseInitialEnergyCallerAssigned.coefficient_norm_le_one line 117
  14. theorem OAI.SevenEighths.InverseInitialEnergyCallerAssigned.assigned_tuple_valid line 132