OAI/Probability/SKFluctuations/Cumulative.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

Cumulative.

  1. def OAI.SKFluctuations.PreKopa.cumulative line 16
  2. theorem OAI.SKFluctuations.PreKopa.hasDerivAt_cumulative line 18
  3. theorem OAI.SKFluctuations.PreKopa.continuous_cumulative line 30
  4. theorem OAI.SKFluctuations.PreKopa.strictMono_cumulative line 34
  5. theorem OAI.SKFluctuations.PreKopa.tendsto_cumulative_atBot line 41
  6. theorem OAI.SKFluctuations.PreKopa.tendsto_cumulative_atTop line 44
  7. theorem OAI.SKFluctuations.PreKopa.cumulative_mem_unitInterval line 48
  8. theorem OAI.SKFluctuations.PreKopa.cumulative_surj_unitInterval line 59
  9. def OAI.SKFluctuations.PreKopa.cumulativeIso line 67
  10. theorem OAI.SKFluctuations.PreKopa.cumulativeIso_apply line 76
  11. def OAI.SKFluctuations.PreKopa.transportIso line 81
  12. theorem OAI.SKFluctuations.PreKopa.cumulative_transport line 87
  13. theorem OAI.SKFluctuations.PreKopa.hasDerivAt_transport line 95
  14. theorem OAI.SKFluctuations.PreKopa.transport_jacobian_bound line 106
  15. theorem OAI.SKFluctuations.PreKopa.prekopaLeindler_normalized line 126
  16. theorem OAI.SKFluctuations.PreKopa.integral_strictlyPositive line 169
  17. theorem OAI.SKFluctuations.PreKopa.prekopaLeindler line 181
  18. def OAI.SKFluctuations.PreKopa.gaussianEnvelope line 207
  19. theorem OAI.SKFluctuations.PreKopa.gaussianEnvelope_cons line 210
  20. theorem OAI.SKFluctuations.PreKopa.gaussianEnvelope_pos line 214
  21. theorem OAI.SKFluctuations.PreKopa.gaussianEnvelope_le_one line 217
  22. theorem OAI.SKFluctuations.PreKopa.integrable_gaussianEnvelope line 223
  23. theorem OAI.SKFluctuations.PreKopa.continuous_cons line 227
  24. def OAI.SKFluctuations.PreKopa.GaussianDominated line 238
  25. theorem OAI.SKFluctuations.PreKopa.GaussianDominated.integrable line 241
  26. theorem OAI.SKFluctuations.PreKopa.GaussianDominated.slice line 247
  27. def OAI.SKFluctuations.PreKopa.firstMarginal line 255
  28. theorem OAI.SKFluctuations.PreKopa.GaussianDominated.continuous_firstMarginal line 258
  29. theorem OAI.SKFluctuations.PreKopa.GaussianDominated.integral_firstMarginal line 285
  30. theorem OAI.SKFluctuations.PreKopa.GaussianDominated.firstMarginal_bound line 302
  31. theorem OAI.SKFluctuations.PreKopa.GaussianDominated.integrable_firstMarginal line 316
  32. theorem OAI.SKFluctuations.PreKopa.integral_finZero line 325
  33. theorem OAI.SKFluctuations.PreKopa.prekopaLeindler_fin line 334
  34. def OAI.SKFluctuations.PreKopa.LogConcave line 364
  35. theorem OAI.SKFluctuations.PreKopa.logConcave_exp_neg line 368
  36. theorem OAI.SKFluctuations.PreKopa.logConcave_marginal line 378
  37. theorem OAI.SKFluctuations.PreKopa.logConcave_integral_exp_neg line 393
  38. theorem OAI.SKFluctuations.PreKopa.LogConcave.of_tendsto line 400
  39. def OAI.SKFluctuations.PreKopa.epigraphPotential line 414
  40. theorem OAI.SKFluctuations.PreKopa.convexOn_epigraphPotential line 419
  41. theorem OAI.SKFluctuations.PreKopa.epigraph_exponential_bound line 460
  42. theorem OAI.SKFluctuations.PreKopa.gaussianDominated_epigraphApprox line 483
  43. def OAI.SKFluctuations.PreKopa.epigraphMarginal line 492
  44. theorem OAI.SKFluctuations.PreKopa.tendsto_epigraphApprox line 497
  45. theorem OAI.SKFluctuations.PreKopa.logConcave_epigraphMarginal line 533
  46. def OAI.SKFluctuations.PreKopa.standardGaussianPDF line 550
  47. theorem OAI.SKFluctuations.PreKopa.standardGaussianPDF_nonneg line 553
  48. theorem OAI.SKFluctuations.PreKopa.integrable_standardGaussianPDF line 556
  49. theorem OAI.SKFluctuations.PreKopa.standardGaussian_pi_withDensity line 561
  50. theorem OAI.SKFluctuations.PreKopa.standardGaussianPDF_eq line 579
  51. theorem OAI.SKFluctuations.PreKopa.LogConcave.const_mul line 591
  52. def OAI.SKFluctuations.PreKopa.finiteEpigraphMarginal line 603
  53. theorem OAI.SKFluctuations.PreKopa.logConcave_finiteEpigraphMarginal line 607
  54. def OAI.SKFluctuations.PreKopa.gaussianEpigraphTilt line 644
  55. theorem OAI.SKFluctuations.PreKopa.gaussianEpigraphTilt_eq line 649
  56. theorem OAI.SKFluctuations.PreKopa.logConcave_gaussianEpigraphTilt line 681