OAI/Combinatorics/BalancedRyser/Deletion/SelectedDeletionKernel.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Balanced.SelectedDeletion.FixedLaw line 15
  2. theorem OAI.Balanced.SelectedDeletion.occupancy_mono line 29
  3. def OAI.Balanced.SelectedDeletion.FixedLaw.relax line 38
  4. def OAI.Balanced.SelectedDeletion.glue line 64
  5. theorem OAI.Balanced.SelectedDeletion.glue_isExperiment line 71
  6. theorem OAI.Balanced.SelectedDeletion.glue_fixedSuccessMass line 89
  7. theorem OAI.Balanced.SelectedDeletion.glue_fixedCylinderMass_le line 93
  8. theorem OAI.Balanced.SelectedDeletion.offset_sum_real line 103
  9. theorem OAI.Balanced.SelectedDeletion.offsetEventProbability_eq_sum line 110
  10. theorem OAI.Balanced.SelectedDeletion.glue_occupancyFailureMass_le line 122
  11. theorem OAI.Balanced.SelectedDeletion.glue_successMass_lower line 140
  12. theorem OAI.Balanced.SelectedDeletion.glue_successMass_lower_half line 156
  13. theorem OAI.Balanced.SelectedDeletion.exists_kernel_of_fixedLaws line 168