OAI/NumberTheory/DirichletL/Inversion/CanonicalShortAttachment.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.InverseCanonicalShortAttachment.idealLists line 16
  2. def OAI.SevenEighths.InverseCanonicalShortAttachment.transportCoeff line 20
  3. theorem OAI.SevenEighths.InverseCanonicalShortAttachment.transportCoeff_val line 24
  4. def OAI.SevenEighths.InverseCanonicalShortAttachment.idealWeights line 28
  5. lemma OAI.SevenEighths.InverseCanonicalShortAttachment.tuple_mark_product line 32
  6. theorem OAI.SevenEighths.InverseCanonicalShortAttachment.indexed_mark_eq_tuple line 47
  7. lemma OAI.SevenEighths.InverseCanonicalShortAttachment.idealLists_disjoint line 65
  8. lemma OAI.SevenEighths.InverseCanonicalShortAttachment.idealLists_prime_data line 78
  9. lemma OAI.SevenEighths.InverseCanonicalShortAttachment.idealLists_capacity line 86
  10. lemma OAI.SevenEighths.InverseCanonicalShortAttachment.idealWeights_norm line 94
  11. def OAI.SevenEighths.InverseCanonicalShortAttachment.longReopened line 104
  12. theorem OAI.SevenEighths.InverseCanonicalShortAttachment.complete_pool_split line 107
  13. lemma OAI.SevenEighths.InverseCanonicalShortAttachment.complete_pool_sub_long line 132
  14. lemma OAI.SevenEighths.InverseCanonicalShortAttachment.primary_span line 148
  15. lemma OAI.SevenEighths.InverseCanonicalShortAttachment.actual_mask line 151
  16. theorem OAI.SevenEighths.InverseCanonicalShortAttachment.normalized_complete_short_attachment line 154