OAI/Probability/SKFluctuations/StandardCompletedLawIsOpenPos.lean

GitHub source file

71 declarations, 0 contain sorry, 0 declared as axioms

Standard Completed Law Is Open Pos.

  1. instance OAI.SKFluctuations.standardCompletedLaw_isOpenPos line 17
  2. theorem OAI.SKFluctuations.liftedFreeEnergy_surjective line 23
  3. theorem OAI.SKFluctuations.augmentedDensity_pos line 36
  4. theorem OAI.SKFluctuations.continuous_augmentedDensity line 60
  5. theorem OAI.SKFluctuations.integrable_augmentedDensity line 64
  6. theorem OAI.SKFluctuations.lintegral_augmentedDensity line 75
  7. theorem OAI.SKFluctuations.integral_augmentedDensity line 81
  8. structure OAI.SKFluctuations.PreKopa.Density line 93
  9. def OAI.SKFluctuations.PreKopa.Density.law line 102
  10. theorem OAI.SKFluctuations.PreKopa.Density.continuous line 104
  11. instance OAI.SKFluctuations.PreKopa.Density.law_probability line 106
  12. instance OAI.SKFluctuations.PreKopa.Density.law_openPos line 113
  13. theorem OAI.SKFluctuations.PreKopa.Density.setIntegral_eq_measureReal line 119
  14. def OAI.SKFluctuations.PreKopa.Density.survival line 125
  15. theorem OAI.SKFluctuations.PreKopa.Density.survival_eq_integral line 127
  16. theorem OAI.SKFluctuations.PreKopa.Density.survival_pos line 131
  17. theorem OAI.SKFluctuations.PreKopa.Density.survival_le_one line 136
  18. theorem OAI.SKFluctuations.PreKopa.Density.lc_survival line 138
  19. theorem OAI.SKFluctuations.PreKopa.Density.concave_log_survival line 142
  20. theorem OAI.SKFluctuations.PreKopa.logConcave_secant line 148
  21. def OAI.SKFluctuations.PreKopa.tailRate line 158
  22. theorem OAI.SKFluctuations.PreKopa.tailRate_pos line 160
  23. theorem OAI.SKFluctuations.PreKopa.survival_tail_from_anchors line 163
  24. def OAI.SKFluctuations.PreKopa.Density.reflect line 211
  25. theorem OAI.SKFluctuations.PreKopa.Density.law_reflect line 223
  26. theorem OAI.SKFluctuations.PreKopa.Density.variance_pos line 235
  27. def OAI.SKFluctuations.PreKopa.Density.mean line 246
  28. def OAI.SKFluctuations.PreKopa.Density.sd line 247
  29. theorem OAI.SKFluctuations.PreKopa.Density.sd_pos line 249
  30. theorem OAI.SKFluctuations.PreKopa.Density.chebyshev_two line 252
  31. theorem OAI.SKFluctuations.PreKopa.Density.survival_anchors line 265
  32. theorem OAI.SKFluctuations.PreKopa.Density.survival_tail line 287
  33. theorem OAI.SKFluctuations.PreKopa.Density.memLp_reflect line 297
  34. theorem OAI.SKFluctuations.PreKopa.Density.mean_reflect line 303
  35. theorem OAI.SKFluctuations.PreKopa.Density.sd_reflect line 309
  36. theorem OAI.SKFluctuations.PreKopa.Density.reflect_survival line 316
  37. theorem OAI.SKFluctuations.PreKopa.Density.left_tail line 324
  38. def OAI.SKFluctuations.PreKopa.Density.tailConstant line 331
  39. theorem OAI.SKFluctuations.PreKopa.Density.tailConstant_pos line 333
  40. theorem OAI.SKFluctuations.PreKopa.Density.abs_tail line 335
  41. theorem OAI.SKFluctuations.PreKopa.exponential_integral_of_tail line 366
  42. def OAI.SKFluctuations.PreKopa.Density.smallTilt line 429
  43. theorem OAI.SKFluctuations.PreKopa.Density.smallTilt_pos line 431
  44. theorem OAI.SKFluctuations.PreKopa.Density.exponential_abs_bound line 434
  45. theorem OAI.SKFluctuations.PreKopa.Density.exponential_centered_le line 445
  46. def OAI.SKFluctuations.PreKopa.Density.momentConstant line 458
  47. theorem OAI.SKFluctuations.PreKopa.Density.momentConstant_pos line 460
  48. theorem OAI.SKFluctuations.PreKopa.Density.centered_abs_moment line 465
  49. def OAI.SKFluctuations.PreKopa.Density.standardized line 502
  50. theorem OAI.SKFluctuations.PreKopa.Density.measurable_standardized line 504
  51. theorem OAI.SKFluctuations.PreKopa.Density.integrable_standardized line 508
  52. theorem OAI.SKFluctuations.PreKopa.Density.integral_standardized line 512
  53. theorem OAI.SKFluctuations.PreKopa.Density.standardized_second line 518
  54. theorem OAI.SKFluctuations.PreKopa.Density.standardized_fourth line 531
  55. def OAI.SKFluctuations.PreKopa.Density.momentRadius line 544
  56. theorem OAI.SKFluctuations.PreKopa.Density.momentRadius_pos line 546
  57. theorem OAI.SKFluctuations.PreKopa.Density.momentRadius_ge_one line 550
  58. theorem OAI.SKFluctuations.PreKopa.Density.fourth_over_radius line 554
  59. theorem OAI.SKFluctuations.PreKopa.Density.square_cutoff line 559
  60. theorem OAI.SKFluctuations.PreKopa.Density.standardized_abs_lower line 573
  61. theorem OAI.SKFluctuations.PreKopa.Density.standardized_positive_lower line 589
  62. def OAI.SKFluctuations.PreKopa.Density.positiveThreshold line 600
  63. def OAI.SKFluctuations.PreKopa.Density.positiveMass line 601
  64. theorem OAI.SKFluctuations.PreKopa.Density.positiveThreshold_pos line 603
  65. theorem OAI.SKFluctuations.PreKopa.Density.positiveMass_pos line 607
  66. theorem OAI.SKFluctuations.PreKopa.Density.positive_cutoff line 611
  67. theorem OAI.SKFluctuations.PreKopa.Density.standardized_positive_mass line 627
  68. theorem OAI.SKFluctuations.PreKopa.Density.positive_mass line 667
  69. theorem OAI.SKFluctuations.PreKopa.Density.centered_mgf_lower line 672
  70. theorem OAI.SKFluctuations.PreKopa.Density.centered_log_mgf_lower line 693
  71. theorem OAI.SKFluctuations.PreKopa.Density.centered_log_mgf_small line 701