OAI/Combinatorics/BalancedRyser/Incidence/AlignedGlobalProjectedIncidence.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Balanced.Local.AlignedGlobal.ProjectionData line 14
  2. def OAI.Balanced.Local.AlignedGlobal.projectionOffsets line 17
  3. def OAI.Balanced.Local.AlignedGlobal.projectionFree line 21
  4. def OAI.Balanced.Local.AlignedGlobal.projectionObservation line 26
  5. theorem OAI.Balanced.Local.AlignedGlobal.projection_point_eq line 34
  6. theorem OAI.Balanced.Local.AlignedGlobal.projection_joint_law line 56
  7. theorem OAI.Balanced.Local.AlignedGlobal.global_projected_left_probability_le_two_div line 69
  8. theorem OAI.Balanced.Local.AlignedGlobal.global_projected_right_probability_le_two_div line 104