OAI/NumberTheory/DirichletL/Moments/AllocatedRayDictionary.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.CenteredMomentAllocatedRayDictionary.originalEmbedding line 20
  2. def OAI.SevenEighths.CenteredMomentAllocatedRayDictionary.remaining line 24
  3. def OAI.SevenEighths.CenteredMomentAllocatedRayDictionary.originalImage line 31
  4. lemma OAI.SevenEighths.CenteredMomentAllocatedRayDictionary.projection_injective line 37
  5. lemma OAI.SevenEighths.CenteredMomentAllocatedRayDictionary.mem_originalImage line 45
  6. lemma OAI.SevenEighths.CenteredMomentAllocatedRayDictionary.originalImage_card line 53
  7. def OAI.SevenEighths.CenteredMomentAllocatedRayDictionary.commonFirst line 59
  8. def OAI.SevenEighths.CenteredMomentAllocatedRayDictionary.commonSecond line 63
  9. lemma OAI.SevenEighths.CenteredMomentAllocatedRayDictionary.commonFirst_pos line 68
  10. lemma OAI.SevenEighths.CenteredMomentAllocatedRayDictionary.commonSecond_pos line 76
  11. structure OAI.SevenEighths.CenteredMomentAllocatedRayDictionary.Matches line 88
  12. lemma OAI.SevenEighths.CenteredMomentAllocatedRayDictionary.common_coefficient line 104
  13. lemma OAI.SevenEighths.CenteredMomentAllocatedRayDictionary.common_height_coefficient line 115
  14. lemma OAI.SevenEighths.CenteredMomentAllocatedRayDictionary.scale_phase_norm line 131
  15. theorem OAI.SevenEighths.CenteredMomentAllocatedRayDictionary.common_energy line 135
  16. theorem OAI.SevenEighths.CenteredMomentAllocatedRayDictionary.common_clipped_energy line 181
  17. theorem OAI.SevenEighths.CenteredMomentAllocatedRayDictionary.both_common_rectangles line 204
  18. lemma OAI.SevenEighths.CenteredMomentAllocatedRayDictionary.deleted_clipped_scale_pos line 235
  19. lemma OAI.SevenEighths.CenteredMomentAllocatedRayDictionary.originalImage_fixedQ line 243
  20. lemma OAI.SevenEighths.CenteredMomentAllocatedRayDictionary.originalImage_bounds line 251
  21. lemma OAI.SevenEighths.CenteredMomentAllocatedRayDictionary.originalImage_scale_bounds line 264