OAI/Probability/CriticalPercolation/Criticality/Weight.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CriticalPercolation.Sharpness.weight line 19
  2. lemma OAI.CriticalPercolation.Sharpness.weight_sum line 21
  3. lemma OAI.CriticalPercolation.Sharpness.weight_nonneg line 24
  4. lemma OAI.CriticalPercolation.Sharpness.weight_eq_bitWeight line 28
  5. lemma OAI.CriticalPercolation.Sharpness.hasDerivAt_weight line 31
  6. lemma OAI.CriticalPercolation.Sharpness.hasDerivAt_density line 38
  7. lemma OAI.CriticalPercolation.Sharpness.density_score line 46
  8. lemma OAI.CriticalPercolation.Sharpness.hasDerivAt_expect_score line 56
  9. lemma OAI.CriticalPercolation.Sharpness.expect_eval_indicator line 71
  10. lemma OAI.CriticalPercolation.Sharpness.expect_coordinate_mask line 87
  11. lemma OAI.CriticalPercolation.Sharpness.score_eq_difference line 117
  12. theorem OAI.CriticalPercolation.Sharpness.hasDerivAt_expect line 143
  13. def OAI.CriticalPercolation.Sharpness.probability line 150
  14. def OAI.CriticalPercolation.Sharpness.closedPivot line 153
  15. def OAI.CriticalPercolation.Sharpness.pivotal line 156
  16. lemma OAI.CriticalPercolation.Sharpness.force_false_subset_true line 160
  17. lemma OAI.CriticalPercolation.Sharpness.indicator_difference line 171
  18. theorem OAI.CriticalPercolation.Sharpness.hasDerivAt_probability line 180
  19. lemma OAI.CriticalPercolation.Sharpness.closedPivot_iff line 193
  20. lemma OAI.CriticalPercolation.Sharpness.probability_closedPivot line 204
  21. theorem OAI.CriticalPercolation.Sharpness.hasDerivAt_probability_closedPivot line 232
  22. lemma OAI.CriticalPercolation.Sharpness.probability_nonneg line 241
  23. lemma OAI.CriticalPercolation.Sharpness.probability_le_one line 249