OAI/Probability/Contingency/DenseRegularity.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

Dense Regularity.

  1. theorem OAI.Contingency.Dense.scaled_affine line 16
  2. theorem OAI.Contingency.Dense.normalized_affine line 28
  3. theorem OAI.Contingency.Dense.polytope_convex line 35
  4. def OAI.Contingency.Dense.coefficient line 43
  5. theorem OAI.Contingency.Dense.normalized_difference line 51
  6. theorem OAI.Contingency.Dense.normalized_width_bound line 71
  7. theorem OAI.Contingency.Dense.coefficient_bound line 80
  8. theorem OAI.Contingency.Dense.normalized_lipschitz line 106
  9. def OAI.Contingency.Dense.penalty line 141
  10. theorem OAI.Contingency.Dense.penalty_nonneg line 146
  11. theorem OAI.Contingency.Dense.le_penalty line 150
  12. theorem OAI.Contingency.Dense.penalty_le_iff line 156
  13. theorem OAI.Contingency.Dense.penalty_convex line 162
  14. theorem OAI.Contingency.Dense.penalty_zero_of_slack line 177
  15. theorem OAI.Contingency.Dense.penalty_difference line 184
  16. def OAI.Contingency.Dense.density line 204
  17. theorem OAI.Contingency.Dense.density_pos line 208
  18. theorem OAI.Contingency.Dense.density_logconcave line 212
  19. structure OAI.Contingency.Interpolation.OpenBox line 235
  20. def OAI.Contingency.Interpolation.OpenBox.carrier line 239
  21. def OAI.Contingency.Interpolation.boxUnion line 242
  22. def OAI.Contingency.Interpolation.FiniteBoxInterpolation line 247
  23. theorem OAI.Contingency.Interpolation.mem_boxUnion line 271
  24. theorem OAI.Contingency.Interpolation.OpenBox.isOpen line 275
  25. theorem OAI.Contingency.Interpolation.OpenBox.isBounded line 278
  26. theorem OAI.Contingency.Interpolation.boxUnion_isOpen line 281
  27. theorem OAI.Contingency.Interpolation.boxUnion_isBounded line 284
  28. theorem OAI.Contingency.Interpolation.boxUnion_measurable line 293
  29. theorem OAI.Contingency.Interpolation.boxUnion_volume_finite line 296
  30. theorem OAI.Contingency.Interpolation.boxUnion_volume_pos line 299
  31. def OAI.Contingency.Interpolation.OpenBox.tail line 302
  32. def OAI.Contingency.Interpolation.slices line 305
  33. theorem OAI.Contingency.Interpolation.mem_slices line 309
  34. def OAI.Contingency.Interpolation.endpoints line 319
  35. theorem OAI.Contingency.Interpolation.lower_mem_endpoints line 323
  36. theorem OAI.Contingency.Interpolation.upper_mem_endpoints line 329
  37. structure OAI.Contingency.Interpolation.GoodWeight line 337
  38. theorem OAI.Contingency.Interpolation.GoodWeight.integrable line 346
  39. theorem OAI.Contingency.Interpolation.GoodWeight.integral_nonneg line 351
  40. theorem OAI.Contingency.Interpolation.GoodWeight.integral_pos line 354
  41. def OAI.Contingency.Interpolation.GoodWeight.slice line 361
  42. theorem OAI.Contingency.Interpolation.GoodWeight.marginal_continuous line 367
  43. def OAI.Contingency.Interpolation.marginal line 392
  44. theorem OAI.Contingency.Interpolation.marginal_nonneg line 395
  45. theorem OAI.Contingency.Interpolation.marginal_fubini line 399
  46. def OAI.Contingency.Interpolation.nextEndpoint line 441
  47. theorem OAI.Contingency.Interpolation.nextEndpoint_le line 444
  48. theorem OAI.Contingency.Interpolation.nextEndpoint_gt line 451
  49. theorem OAI.Contingency.Interpolation.nextEndpoint_mem line 458
  50. theorem OAI.Contingency.Interpolation.endpoint_not_between line 466
  51. theorem OAI.Contingency.Interpolation.endpoint_comparisons line 473
  52. theorem OAI.Contingency.Interpolation.grid_covers line 482
  53. theorem OAI.Contingency.Interpolation.interval_inverse line 513
  54. theorem OAI.Contingency.Interpolation.positive_quantile line 553
  55. theorem OAI.Contingency.Interpolation.transport_amgm line 599
  56. def OAI.Contingency.Interpolation.prefixMass line 623
  57. def OAI.Contingency.Interpolation.totalMass line 626
  58. theorem OAI.Contingency.Interpolation.prefix_nonneg line 628
  59. theorem OAI.Contingency.Interpolation.prefix_next_le line 631
  60. theorem OAI.Contingency.Interpolation.prefix_add_le_total line 645
  61. def OAI.Contingency.Interpolation.probabilityPiece line 654
  62. theorem OAI.Contingency.Interpolation.probabilityPiece_subset line 657
  63. theorem OAI.Contingency.Interpolation.probabilityPiece_disjoint line 663
  64. theorem OAI.Contingency.Interpolation.probabilityPieces_volume line 678