OAI/NumberTheory/DirichletL/Dictionary/InverseAssignedCount.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.DetectorDictionaryInverseAssignedCount.assignedTuples line 11
  2. theorem OAI.SevenEighths.DetectorDictionaryInverseAssignedCount.mem_assignedTuples line 14
  3. def OAI.SevenEighths.DetectorDictionaryInverseAssignedCount.assignedConstant line 19
  4. theorem OAI.SevenEighths.DetectorDictionaryInverseAssignedCount.assignedConstant_pos line 21
  5. theorem OAI.SevenEighths.DetectorDictionaryInverseAssignedCount.list_card_le line 26
  6. theorem OAI.SevenEighths.DetectorDictionaryInverseAssignedCount.assigned_card_le line 35
  7. def OAI.SevenEighths.DetectorDictionaryInverseAssignedCount.assignedCoefficient line 56
  8. theorem OAI.SevenEighths.DetectorDictionaryInverseAssignedCount.assignedCoefficient_norm_le_one line 59
  9. theorem OAI.SevenEighths.DetectorDictionaryInverseAssignedCount.restricted_mass_le line 68
  10. theorem OAI.SevenEighths.DetectorDictionaryInverseAssignedCount.restricted_normalized_mass_le line 83
  11. theorem OAI.SevenEighths.DetectorDictionaryInverseAssignedCount.restricted_sum_normalized_le line 98
  12. theorem OAI.SevenEighths.DetectorDictionaryInverseAssignedCount.slots_normalized_mass_le line 109
  13. theorem OAI.SevenEighths.DetectorDictionaryInverseAssignedCount.assigned_sum_normalized_le line 123
  14. theorem OAI.SevenEighths.DetectorDictionaryInverseAssignedCount.slots_card_le line 132
  15. theorem OAI.SevenEighths.DetectorDictionaryInverseAssignedCount.assignedTuples_eq_empty line 143
  16. theorem OAI.SevenEighths.DetectorDictionaryInverseAssignedCount.assignedTuples_card_of_isEmpty line 151