OAI/Probability/Contingency/DenseAnalytic.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

Dense Analytic.

  1. theorem OAI.Contingency.Dense.normalized_continuous line 18
  2. theorem OAI.Contingency.Dense.penalty_continuous line 25
  3. theorem OAI.Contingency.Dense.density_continuous line 31
  4. theorem OAI.Contingency.Dense.density_le_one line 36
  5. def OAI.Contingency.Dense.densityWeight line 41
  6. theorem OAI.Contingency.Dense.densityWeight_logconcave line 50
  7. theorem OAI.Contingency.Interpolation.mix_contains line 65
  8. theorem OAI.Contingency.Interpolation.mass_gain line 75
  9. def OAI.Contingency.Dense.region line 117
  10. theorem OAI.Contingency.Dense.region_measurable line 120
  11. theorem OAI.Contingency.Dense.homothety_affine line 127
  12. theorem OAI.Contingency.Dense.inner_image_subset line 138
  13. theorem OAI.Contingency.Dense.relaxed_subset_image line 148
  14. theorem OAI.Contingency.Dense.homothety_volume line 175
  15. theorem OAI.Contingency.Dense.inner_volume line 181
  16. theorem OAI.Contingency.Dense.relaxed_volume line 190
  17. def OAI.Contingency.Dense.constraints line 215
  18. theorem OAI.Contingency.Dense.constraints_affine line 219
  19. theorem OAI.Contingency.Dense.constraints_continuous line 224
  20. theorem OAI.Contingency.Dense.constraints_lipschitz line 228
  21. theorem OAI.Contingency.Dense.region_bounded line 241
  22. theorem OAI.Contingency.Dense.region_volume_finite line 251
  23. theorem OAI.Contingency.Dense.region_interior line 259
  24. theorem OAI.Contingency.Dense.inner_half_volume line 268
  25. theorem OAI.Contingency.Dense.relaxed_volume_dense line 300
  26. theorem OAI.Contingency.Dense.half_times_four_thirds line 325
  27. theorem OAI.Contingency.Dense.geometric_constant line 329
  28. theorem OAI.Contingency.Dense.decay_nat line 338
  29. theorem OAI.Contingency.Dense.density_layer_bound line 345
  30. theorem OAI.Contingency.Dense.exp_quarter_bound line 388
  31. theorem OAI.Contingency.Dense.dense_exponent_layer line 394
  32. def OAI.Contingency.Grid.inside line 433
  33. def OAI.Contingency.Grid.path line 436
  34. theorem OAI.Contingency.Grid.path_zero line 439
  35. theorem OAI.Contingency.Grid.path_end line 440
  36. theorem OAI.Contingency.Grid.exists_label_step line 442
  37. theorem OAI.Contingency.Grid.path_step line 452
  38. def OAI.Contingency.Grid.neighbors line 461
  39. def OAI.Contingency.Grid.face line 465
  40. theorem OAI.Contingency.Grid.adjacent_of_close line 468
  41. theorem OAI.Contingency.Grid.cut_face_close line 481
  42. abbrev OAI.Contingency.Grid.Vertex line 549
  43. def OAI.Contingency.Grid.corner line 551
  44. def OAI.Contingency.Grid.bin line 553
  45. theorem OAI.Contingency.Grid.mem_bin line 556
  46. def OAI.Contingency.Grid.cube line 559
  47. theorem OAI.Contingency.Grid.mem_cube line 561
  48. def OAI.Contingency.Grid.boxes line 564
  49. theorem OAI.Contingency.Grid.mem_boxes line 566
  50. theorem OAI.Contingency.Grid.bins_subset_cube line 571
  51. theorem OAI.Contingency.Grid.bin_unique line 579
  52. theorem OAI.Contingency.Grid.bins_disjoint line 596
  53. theorem OAI.Contingency.Grid.ae_no_grid line 603
  54. theorem OAI.Contingency.Grid.exists_bin line 610
  55. theorem OAI.Contingency.Grid.cube_ae_union line 622
  56. def OAI.Contingency.Grid.faceBox line 633
  57. theorem OAI.Contingency.Grid.mem_faceBox line 637
  58. theorem OAI.Contingency.Grid.bounded_cut_face line 655