OAI/Combinatorics/SumProduct/Alignment/RoughFace02.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RoughFaceShift.fullDomain line 22
  2. def OAI.RoughFaceShift.labelExposure line 25
  3. structure OAI.RoughFaceShift.FaceData line 33
  4. def OAI.RoughFaceShift.FaceData.Valid line 39
  5. def OAI.RoughFaceShift.rawFaceEvent line 49
  6. lemma OAI.RoughFaceShift.joint_ae_fullDomain line 68
  7. lemma OAI.RoughFaceShift.joint_restrict_fullDomain line 80
  8. lemma OAI.RoughFaceShift.emod_unit line 89
  9. lemma OAI.RoughFaceShift.image_residues line 101
  10. lemma OAI.RoughFaceShift.label_exposure_legal line 119
  11. lemma OAI.RoughFaceShift.good_preimages line 170
  12. lemma OAI.RoughFaceShift.real_support_restrict line 202
  13. lemma OAI.RoughFaceShift.singleton_event_sum line 209
  14. lemma OAI.RoughFaceShift.supported_partition_lower line 220
  15. lemma OAI.RoughFaceShift.supported_conditional_bad_bound line 249