OAI/Probability/CriticalPercolation/Entropy/FreshSet.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CriticalPercolation.Priority.freshSet line 23
  2. lemma OAI.CriticalPercolation.Priority.measurableSet_freshSet line 27
  3. lemma OAI.CriticalPercolation.Priority.integrable_eval_continuous line 37
  4. lemma OAI.CriticalPercolation.Priority.integral_freshSet line 42
  5. lemma OAI.CriticalPercolation.Priority.uniform01_integral_eq_interval line 72
  6. lemma OAI.CriticalPercolation.Priority.weighted_fresh_identity line 79
  7. lemma OAI.CriticalPercolation.Priority.square_weight_integral line 86
  8. def OAI.CriticalPercolation.Priority.enumeration line 99
  9. abbrev OAI.CriticalPercolation.Priority.Order line 101
  10. instance OAI.CriticalPercolation.Priority.(instance at line 103) line 103
  11. lemma OAI.CriticalPercolation.Priority.order_nodup line 108
  12. lemma OAI.CriticalPercolation.Priority.mem_order line 111
  13. def OAI.CriticalPercolation.Priority.cell line 115
  14. lemma OAI.CriticalPercolation.Priority.measurableSet_pairwise line 119
  15. lemma OAI.CriticalPercolation.Priority.measurableSet_cell line 138
  16. lemma OAI.CriticalPercolation.Priority.exists_cell line 141
  17. lemma OAI.CriticalPercolation.Priority.cell_disjoint line 154
  18. lemma OAI.CriticalPercolation.Priority.order_split line 162
  19. lemma OAI.CriticalPercolation.Priority.before_iff line 172