OAI/Combinatorics/SumProduct/Alignment/RoughArray03.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RoughArrayCoordinates.badPhysical line 17
  2. theorem OAI.RoughArrayCoordinates.badPhysical_subset line 39
  3. def OAI.RoughArrayCoordinates.rStar line 82
  4. def OAI.RoughArrayCoordinates.yStar line 86
  5. def OAI.RoughArrayCoordinates.coarseOrigin line 88
  6. def OAI.RoughArrayCoordinates.physicalOrigin line 92
  7. def OAI.RoughArrayCoordinates.rawPhysicalEvent line 98
  8. lemma OAI.RoughArrayCoordinates.scalar_origin_bound line 115
  9. lemma OAI.RoughArrayCoordinates.rStar_expose line 150
  10. lemma OAI.RoughArrayCoordinates.physicalOrigin_div line 160
  11. lemma OAI.RoughArrayCoordinates.physicalOrigin_bound line 201
  12. lemma OAI.RoughArrayCoordinates.rawPhysical_subset line 249