OAI/NumberTheory/DirichletL/Descent/SecondAssignedSource.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.InverseMoment.pairedSlotAssignment line 13
  2. theorem OAI.SevenEighths.InverseMoment.pairedSlotAssignment_injective line 18
  3. def OAI.SevenEighths.InverseMoment.pairedSlotWeight line 29
  4. theorem OAI.SevenEighths.InverseMoment.paired_primeMark_assignments line 33
  5. theorem OAI.SevenEighths.InverseMoment.pairedSlotWeight_norm_le_one line 42
  6. def OAI.SevenEighths.InverseMoment.attachSecondSlots line 54
  7. theorem OAI.SevenEighths.InverseMoment.attachSecondSlots_injective line 65
  8. def OAI.SevenEighths.InverseMoment.attachPairedSlots line 79
  9. theorem OAI.SevenEighths.InverseMoment.attachPairedSlots_injective line 85
  10. def OAI.SevenEighths.InverseMoment.assignedSecondSource line 94
  11. theorem OAI.SevenEighths.InverseMoment.mem_assignedSecondSource line 101
  12. theorem OAI.SevenEighths.InverseMoment.assignedSecondSource_conditions line 133