OAI/Probability/SignedSweeps/HoleEntropy.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SignedSweeps.occupancy line 10
  2. lemma OAI.SignedSweeps.occupancy_sum line 15
  3. lemma OAI.SignedSweeps.occupancy_at_pos line 20
  4. lemma OAI.SignedSweeps.occupancy_sum_smul line 25
  5. def OAI.SignedSweeps.occupancyEntropy line 29
  6. def OAI.SignedSweeps.empiricalDensity line 32
  7. lemma OAI.SignedSweeps.empiricalDensity_nonneg line 35
  8. lemma OAI.SignedSweeps.empiricalDensity_sum line 38
  9. lemma OAI.SignedSweeps.empiricalDensity_at_pos line 44
  10. lemma OAI.SignedSweeps.empiricalDensity_total line 49
  11. lemma OAI.SignedSweeps.occupancy_entropy_weight line 53
  12. lemma OAI.SignedSweeps.occupancy_entropy_fiber_bound line 80
  13. lemma OAI.SignedSweeps.occupancy_entropy_sum line 109
  14. abbrev OAI.SignedSweeps.HolePlacement line 122
  15. def OAI.SignedSweeps.holeLineEntropy line 125
  16. lemma OAI.SignedSweeps.hole_entropy_with_replacement line 129
  17. lemma OAI.SignedSweeps.hole_entropy_drop_distinctness line 151
  18. lemma OAI.SignedSweeps.inverse_pow_eq_exp_log line 160
  19. lemma OAI.SignedSweeps.hole_assignment_entropy_bound line 164
  20. lemma OAI.SignedSweeps.hole_assignment_entropy_bound_exp line 212