OAI/Probability/SKFluctuations/LowerOnInterval.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

Lower On Interval.

  1. theorem OAI.SKFluctuations.PreKopa.Density.lower_on_interval line 18
  2. theorem OAI.SKFluctuations.PreKopa.Density.point_half_drop line 34
  3. theorem OAI.SKFluctuations.PreKopa.Density.point_right_tail line 52
  4. theorem OAI.SKFluctuations.PreKopa.Density.integrableOn_exp_shift line 85
  5. theorem OAI.SKFluctuations.PreKopa.Density.integral_exp_shift line 96
  6. theorem OAI.SKFluctuations.PreKopa.Density.point_right_survival line 109
  7. def OAI.SKFluctuations.PreKopa.Density.pointTailConstant line 122
  8. theorem OAI.SKFluctuations.PreKopa.Density.pointTailConstant_pos line 124
  9. theorem OAI.SKFluctuations.PreKopa.Density.point_right_survival_all line 128
  10. theorem OAI.SKFluctuations.PreKopa.Density.point_abs_tail line 151
  11. def OAI.SKFluctuations.PreKopa.Density.densityMomentConstant line 177
  12. theorem OAI.SKFluctuations.PreKopa.Density.densityMomentConstant_pos line 179
  13. theorem OAI.SKFluctuations.PreKopa.Density.point_exponential_bound line 183
  14. theorem OAI.SKFluctuations.PreKopa.Density.point_second_moment line 193
  15. def OAI.SKFluctuations.PreKopa.Density.densityBoundConstant line 218
  16. theorem OAI.SKFluctuations.PreKopa.Density.densityBoundConstant_pos line 220
  17. theorem OAI.SKFluctuations.PreKopa.Density.density_bound line 223
  18. theorem OAI.SKFluctuations.PreKopa.Density.interval_mass_bound line 236
  19. def OAI.SKFluctuations.augmentedProbabilityDensity line 255
  20. theorem OAI.SKFluctuations.law_augmentedProbabilityDensity line 263
  21. theorem OAI.SKFluctuations.memLp_augmentedLaw line 267
  22. theorem OAI.SKFluctuations.memLp_augmentedProbabilityDensity line 273
  23. def OAI.SKFluctuations.augmentedSD line 278
  24. theorem OAI.SKFluctuations.sd_augmentedProbabilityDensity line 281
  25. theorem OAI.SKFluctuations.augmentedSD_pos line 287
  26. theorem OAI.SKFluctuations.mean_augmentedProbabilityDensity line 292
  27. theorem OAI.SKFluctuations.integrable_exp_augmentedLaw line 297
  28. theorem OAI.SKFluctuations.integrable_exp_centered_augmentedLaw line 306
  29. theorem OAI.SKFluctuations.augmented_tail line 312
  30. theorem OAI.SKFluctuations.augmented_interval_mass line 320
  31. theorem OAI.SKFluctuations.completed_logLaplace_small line 328
  32. theorem OAI.SKFluctuations.completed_logLaplace_lower line 340
  33. theorem OAI.SKFluctuations.augmentationCorrection_nonneg line 360
  34. theorem OAI.SKFluctuations.augmentationCorrection_le line 366
  35. theorem OAI.SKFluctuations.augmentedSD_lower_of_logLaplace line 373
  36. theorem OAI.SKFluctuations.augmentedSD_upper_of_logLaplace line 386
  37. def OAI.SKFluctuations.PinnedVariance.quadraticTilt line 404
  38. def OAI.SKFluctuations.PinnedVariance.quadraticTilt₁ line 406
  39. def OAI.SKFluctuations.PinnedVariance.quadraticTilt₂ line 408
  40. theorem OAI.SKFluctuations.PinnedVariance.hasDerivAt_quadraticTilt line 411
  41. theorem OAI.SKFluctuations.PinnedVariance.hasDerivAt_quadraticTilt₁ line 419
  42. theorem OAI.SKFluctuations.PinnedVariance.quadraticTilt_bounds line 427
  43. theorem OAI.SKFluctuations.PinnedVariance.integrable_quadraticTilt_all line 462
  44. theorem OAI.SKFluctuations.PinnedVariance.hasDerivAt_integral_quadraticTilt line 475
  45. theorem OAI.SKFluctuations.PinnedVariance.hasDerivAt_integral_quadraticTilt₁ line 494
  46. theorem OAI.SKFluctuations.PinnedVariance.hasDerivAt_log_integral_quadraticTilt line 513
  47. theorem OAI.SKFluctuations.PinnedVariance.hasDerivAt_logSlope_zero line 521
  48. theorem OAI.SKFluctuations.PinnedVariance.variance_le_of_concave_quadraticTilt line 542
  49. theorem OAI.SKFluctuations.PreKopa.concaveOn_log_integral_exp_neg line 568
  50. def OAI.SKFluctuations.PinnedVariance.quadraticPotential line 606
  51. theorem OAI.SKFluctuations.PinnedVariance.gaussianDominated_quadraticPotential line 609
  52. theorem OAI.SKFluctuations.PinnedVariance.variance_le_of_convex_quadraticPotential line 636