OAI/Geometry/TranslativeCovering/FiniteJanson.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FiniteJanson.atom line 54
  2. def OAI.FiniteJanson.prob line 57
  3. theorem OAI.FiniteJanson.atom_nonneg line 62
  4. theorem OAI.FiniteJanson.sum_atom line 68
  5. theorem OAI.FiniteJanson.prob_nonneg line 73
  6. theorem OAI.FiniteJanson.prob_univ line 81
  7. theorem OAI.FiniteJanson.prob_empty line 84
  8. theorem OAI.FiniteJanson.prob_mono line 87
  9. theorem OAI.FiniteJanson.prob_compl line 98
  10. theorem OAI.FiniteJanson.prob_inter_compl line 107
  11. theorem OAI.FiniteJanson.atom_lattice line 116
  12. def OAI.FiniteJanson.ind line 125
  13. theorem OAI.FiniteJanson.prob_eq line 128
  14. theorem OAI.FiniteJanson.ind_nonneg line 135
  15. theorem OAI.FiniteJanson.ind_mono line 141
  16. theorem OAI.FiniteJanson.harris line 148
  17. theorem OAI.FiniteJanson.harris_opposite line 161
  18. theorem OAI.FiniteJanson.atom_split line 168
  19. theorem OAI.FiniteJanson.prob_split line 174
  20. def OAI.FiniteJanson.Supported line 210
  21. theorem OAI.FiniteJanson.prob_independent line 213
  22. def OAI.FiniteJanson.occurs line 243
  23. theorem OAI.FiniteJanson.occurs_upper line 246
  24. theorem OAI.FiniteJanson.occurs_supported line 253
  25. theorem OAI.FiniteJanson.occurs_union line 262
  26. def OAI.FiniteJanson.avoids line 266
  27. theorem OAI.FiniteJanson.avoids_empty line 270
  28. theorem OAI.FiniteJanson.avoids_insert line 275
  29. theorem OAI.FiniteJanson.avoids_lower line 281
  30. theorem OAI.FiniteJanson.avoids_supported_compl line 287
  31. theorem OAI.FiniteJanson.avoids_split line 301
  32. theorem OAI.FiniteJanson.prob_remove_le line 313
  33. theorem OAI.FiniteJanson.avoidance_step line 326
  34. def OAI.FiniteJanson.mean line 393
  35. def OAI.FiniteJanson.offCost line 396
  36. def OAI.FiniteJanson.offSum line 399
  37. theorem OAI.FiniteJanson.offCost_self line 402
  38. theorem OAI.FiniteJanson.offCost_symm line 405
  39. theorem OAI.FiniteJanson.mean_insert line 409
  40. theorem OAI.FiniteJanson.offSum_insert line 413
  41. theorem OAI.FiniteJanson.janson_first line 435
  42. theorem OAI.FiniteJanson.prob_singleton line 447
  43. theorem OAI.FiniteJanson.prob_occurs line 451
  44. theorem OAI.FiniteJanson.atom_sum line 486
  45. theorem OAI.FiniteJanson.prob_sum line 490
  46. def OAI.FiniteJanson.gated line 507
  47. theorem OAI.FiniteJanson.occurs_gated line 511
  48. theorem OAI.FiniteJanson.avoidance_gated_subset line 516
  49. theorem OAI.FiniteJanson.prob_avoidance_le_gated line 521
  50. theorem OAI.FiniteJanson.prob_gated line 538
  51. theorem OAI.FiniteJanson.prob_gated_pair line 544
  52. theorem OAI.FiniteJanson.disjoint_gated line 560
  53. theorem OAI.FiniteJanson.mean_gated line 564
  54. theorem OAI.FiniteJanson.offSum_gated line 569
  55. theorem OAI.FiniteJanson.janson_thinned line 584
  56. def OAI.FiniteJanson.depSum line 596
  57. theorem OAI.FiniteJanson.depSum_eq line 600
  58. theorem OAI.FiniteJanson.mean_nonneg line 619
  59. theorem OAI.FiniteJanson.offSum_nonneg line 622
  60. theorem OAI.FiniteJanson.janson line 633