OAI/Probability/Contingency/PieceQuantiles.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

Piece Quantiles.

  1. structure OAI.Contingency.Interpolation.SourcePieces line 19
  2. def OAI.Contingency.Interpolation.SourcePieces.mass line 31
  3. def OAI.Contingency.Interpolation.SourcePieces.total line 33
  4. theorem OAI.Contingency.Interpolation.SourcePieces.mass_pos line 35
  5. theorem OAI.Contingency.Interpolation.SourcePieces.total_pos line 40
  6. def OAI.Contingency.Interpolation.SourcePieces.good line 45
  7. theorem OAI.Contingency.Interpolation.SourcePieces.good_measurable line 47
  8. theorem OAI.Contingency.Interpolation.SourcePieces.good_subset line 50
  9. theorem OAI.Contingency.Interpolation.SourcePieces.good_volume line 55
  10. theorem OAI.Contingency.Interpolation.SourcePieces.good_ae line 58
  11. theorem OAI.Contingency.Interpolation.SourcePieces.local_quantiles line 65
  12. theorem OAI.Contingency.Interpolation.SourcePieces.quantile line 98
  13. theorem OAI.Contingency.Interpolation.slices_constant line 156
  14. def OAI.Contingency.Interpolation.activeEndpoints line 170
  15. theorem OAI.Contingency.Interpolation.activeEndpoint_mem line 175
  16. theorem OAI.Contingency.Interpolation.activeEndpoint_lt line 180
  17. def OAI.Contingency.Interpolation.gridMidpoint line 186
  18. theorem OAI.Contingency.Interpolation.midpoint_mem line 189
  19. theorem OAI.Contingency.Interpolation.activeSlice_nonempty line 194
  20. def OAI.Contingency.Interpolation.gridLower line 201
  21. theorem OAI.Contingency.Interpolation.gridLower_mem line 204
  22. def OAI.Contingency.Interpolation.boxPieces line 207
  23. theorem OAI.Contingency.Interpolation.boxPieces_slice line 217
  24. theorem OAI.Contingency.Interpolation.boxPieces_cover line 224
  25. def OAI.Contingency.Interpolation.SourcePieces.source line 256
  26. theorem OAI.Contingency.Interpolation.SourcePieces.support_disjoint line 259
  27. theorem OAI.Contingency.Interpolation.SourcePieces.source_on line 266
  28. theorem OAI.Contingency.Interpolation.SourcePieces.source_off line 277
  29. theorem OAI.Contingency.Interpolation.SourcePieces.piece_integrable line 280
  30. theorem OAI.Contingency.Interpolation.SourcePieces.source_integrable line 284
  31. theorem OAI.Contingency.Interpolation.SourcePieces.source_integral line 287
  32. theorem OAI.Contingency.Interpolation.boxPieces_source_eq line 312
  33. theorem OAI.Contingency.Interpolation.boxPieces_source_ae line 329
  34. theorem OAI.Contingency.Interpolation.boxPieces_total line 336
  35. theorem OAI.Contingency.Interpolation.activeEndpoints_nonempty line 341
  36. theorem OAI.Contingency.Interpolation.piece_interpolation line 366
  37. theorem OAI.Contingency.Interpolation.cons_interpolation line 438
  38. theorem OAI.Contingency.Interpolation.good_box_interpolation line 445
  39. def OAI.Contingency.Interpolation.clampBox line 509
  40. theorem OAI.Contingency.Interpolation.clampBox_mem line 511
  41. theorem OAI.Contingency.Interpolation.clampBox_eq line 517
  42. theorem OAI.Contingency.Interpolation.clampBox_continuous line 521
  43. theorem OAI.Contingency.Interpolation.good_extension line 526
  44. theorem OAI.Contingency.Interpolation.finiteBoxInterpolation line 538
  45. def OAI.Contingency.Interpolation.OpenBox.proper line 581
  46. def OAI.Contingency.Interpolation.OpenBox.mix line 583
  47. theorem OAI.Contingency.Interpolation.OpenBox.proper_of_mem line 586
  48. theorem OAI.Contingency.Interpolation.interval_mix line 589
  49. theorem OAI.Contingency.Interpolation.OpenBox.mem_mix_iff line 606
  50. def OAI.Contingency.Interpolation.mixBoxes line 622
  51. theorem OAI.Contingency.Interpolation.mem_mixBoxes line 626
  52. theorem OAI.Contingency.Interpolation.logconcave_interpolation line 639