OAI/Combinatorics/BalancedRyser/Probability/TailConditioning2.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.TailConditioning.minSlotSize_le line 21
  2. theorem OAI.Balanced.TailConditioning.slotSize_sigma line 28
  3. theorem OAI.Balanced.TailConditioning.eight_mul_degree_le_min line 42
  4. theorem OAI.Balanced.TailConditioning.conditionalCylinder_eq_zero line 53
  5. theorem OAI.Balanced.TailConditioning.independentTransversals_eq_avoid line 68
  6. theorem OAI.Balanced.TailConditioning.graph_nonneighbor_independence line 90
  7. theorem OAI.Balanced.TailConditioning.graph_cylinder_independence line 110
  8. theorem OAI.Balanced.TailConditioning.tail_conditioning_of_bounds line 128
  9. theorem OAI.Balanced.TailConditioning.tail_conditioning line 196
  10. theorem OAI.Balanced.TailConditioning.tail_conditioning_of_pointwise_bounds line 213
  11. theorem OAI.Balanced.TailConditioning.conditionalCylinder_eq_cond_real line 243
  12. theorem OAI.Balanced.TailConditioning.conditionalCylinder_eq_zero_of_no_realization line 254