OAI/Combinatorics/BalancedRyser/Local/LocalTwoReuseAssembly.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.Local.TwoReuseAssembly.offsetProbability_mono line 15
  2. theorem OAI.Balanced.Local.TwoReuseAssembly.offsetProbability_nonneg line 26
  3. theorem OAI.Balanced.Local.TwoReuseAssembly.cross_count_scale_le line 31
  4. theorem OAI.Balanced.Local.TwoReuseAssembly.noninjective_joint_sum_le line 55
  5. theorem OAI.Balanced.Local.TwoReuseAssembly.injective_joint_sum_le_of_conditional line 98
  6. theorem OAI.Balanced.Local.TwoReuseAssembly.direction_sum_le_of_injective line 143
  7. def OAI.Balanced.Local.TwoReuseAssembly.InjectiveTwoReuseEstimate line 187
  8. theorem OAI.Balanced.Local.TwoReuseAssembly.pencilTwoReuses_of_alignment_and_injective line 198