OAI/Geometry/TranslativeCovering/PoissonConfig.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PoissonConfig.Config line 18
  2. def OAI.PoissonConfig.count line 20
  3. lemma OAI.PoissonConfig.measurableSet_sigma line 23
  4. lemma OAI.PoissonConfig.measurable_sigma line 28
  5. lemma OAI.PoissonConfig.measurable_count line 36
  6. def OAI.PoissonConfig.witnessCount line 48
  7. lemma OAI.PoissonConfig.measurable_witnessCount line 52
  8. structure OAI.PoissonConfig.IsPoisson line 67
  9. def OAI.PoissonConfig.occupied line 74
  10. lemma OAI.PoissonConfig.measurable_occupied line 77
  11. lemma OAI.PoissonConfig.occupied_independent line 81
  12. lemma OAI.PoissonConfig.count_zero_prob line 95
  13. lemma OAI.PoissonConfig.occupied_prob line 104
  14. structure OAI.PoissonConfig.HasVoidLaw line 115
  15. lemma OAI.PoissonConfig.count_zero_iff line 120
  16. lemma OAI.PoissonConfig.occupied_independent_of_void line 124
  17. lemma OAI.PoissonConfig.occupied_prob_of_void line 151
  18. lemma OAI.PoissonConfig.IsPoisson.hasVoidLaw line 162