OAI/Combinatorics/BalancedRyser/Profiles/ProfilePoissonLemmas.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.profile_recurrence_factorial line 13
  2. theorem OAI.Balanced.profile_recurrence_poisson line 30
  3. theorem OAI.Balanced.profile_recurrence_eq_poissonMeasure line 49
  4. theorem OAI.Balanced.profile_recurrence_factorization line 57
  5. theorem OAI.Balanced.ProfileVisibility.ae_eq_const_of_integral_eq line 75
  6. theorem OAI.Balanced.ProfileVisibility.ae_eq_const_of_probability_integral line 83
  7. theorem OAI.Balanced.ProfileVisibility.recurrence_of_invisible line 91
  8. theorem OAI.Balanced.ProfileVisibility.null_of_vanishes line 106
  9. theorem OAI.Balanced.ProfileVisibility.full_mass_of_vanishes line 116
  10. theorem OAI.Balanced.ProfileVisibility.saturated_coordinate_visible line 128