OAI/Probability/Contingency/GridCover.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

Grid Cover.

  1. theorem OAI.Contingency.Grid.neighbors_symm line 18
  2. theorem OAI.Contingency.Grid.neighbors_unique line 21
  3. theorem OAI.Contingency.Grid.faceBox_swap line 27
  4. def OAI.Contingency.Grid.Cut line 40
  5. instance OAI.Contingency.Grid.cutFintype line 43
  6. def OAI.Contingency.Grid.Cut.coord line 45
  7. theorem OAI.Contingency.Grid.Cut.adjacent line 47
  8. def OAI.Contingency.Grid.Cut.neighborhood line 50
  9. theorem OAI.Contingency.Grid.cut_cover_endpoints line 52
  10. theorem OAI.Contingency.Grid.minkowski_cut_cover line 70
  11. theorem OAI.Contingency.Grid.box_integrable line 115
  12. theorem OAI.Contingency.Grid.bin_volume line 118
  13. theorem OAI.Contingency.Grid.box_volume_real line 121
  14. theorem OAI.Contingency.Grid.faceBox_volume line 128
  15. theorem OAI.Contingency.Grid.integral_boxes line 145
  16. theorem OAI.Contingency.Grid.bin_integral_bounds line 157
  17. theorem OAI.Contingency.Grid.boxes_integral_bounds line 170
  18. theorem OAI.Contingency.Grid.face_volume_bound line 195
  19. theorem OAI.Contingency.Grid.integral_cover line 220
  20. def OAI.Contingency.Grid.border line 262
  21. def OAI.Contingency.Grid.Cut.reverse line 265
  22. theorem OAI.Contingency.Grid.border_compl line 275
  23. theorem OAI.Contingency.Grid.mass_partition line 283
  24. theorem OAI.Contingency.Grid.boxes_nonempty line 290
  25. theorem OAI.Contingency.Grid.face_integral_bound line 298
  26. theorem OAI.Contingency.Grid.small_side_border line 313
  27. theorem OAI.Contingency.Grid.border_bound line 350
  28. def OAI.Contingency.Grid.realCorner line 382
  29. def OAI.Contingency.Grid.exponentWeight line 385
  30. theorem OAI.Contingency.Grid.exponentWeight_pos line 388
  31. theorem OAI.Contingency.Grid.exponentWeight_upper line 391
  32. theorem OAI.Contingency.Grid.exponentWeight_lower line 399
  33. theorem OAI.Contingency.Grid.bin_distance line 407
  34. theorem OAI.Contingency.Grid.face_distance line 416
  35. theorem OAI.Contingency.Grid.weight_bin_comparison line 441
  36. theorem OAI.Contingency.Grid.weight_face_comparison line 452
  37. def OAI.Contingency.Dense.binExponent line 483
  38. def OAI.Contingency.Dense.binWeight line 487
  39. theorem OAI.Contingency.Dense.exponent_lipschitz line 490
  40. theorem OAI.Contingency.Dense.bin_density_eq line 517
  41. theorem OAI.Contingency.Dense.bin_border_bound line 525
  42. theorem OAI.Contingency.Dense.bin_conductance_numerator line 556
  43. theorem OAI.Contingency.Dense.region_volume_pos line 598
  44. theorem OAI.Contingency.Dense.dense_density_volume line 608
  45. theorem OAI.Contingency.Dense.dense_bin_normalizer_bound line 639