OAI/Analysis/Steinitz/Prekopa.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

Prékopa inequalities and Gaussian log-concavity.

  1. lemma OAI.Prekopa.continuousAt_invFun_strictMono line 14
  2. lemma OAI.Prekopa.invFun_hasDerivAt line 43
  3. def OAI.Prekopa.primitive line 55
  4. lemma OAI.Prekopa.primitive_hasDerivAt line 57
  5. lemma OAI.Prekopa.primitive_continuous line 62
  6. lemma OAI.Prekopa.primitive_strictMono line 66
  7. lemma OAI.Prekopa.normalized_interval line 73
  8. lemma OAI.Prekopa.interval line 155
  9. lemma OAI.Prekopa.real line 181
  10. def OAI.Prekopa.gauss line 203
  11. lemma OAI.Prekopa.gauss_prod line 206
  12. lemma OAI.Prekopa.gauss_cons line 210
  13. lemma OAI.Prekopa.gauss_pos line 214
  14. lemma OAI.Prekopa.gauss_le_one line 217
  15. lemma OAI.Prekopa.gauss_integrable line 222
  16. structure OAI.Prekopa.Nice line 226
  17. lemma OAI.Prekopa.Nice.integrable line 231
  18. lemma OAI.Prekopa.continuous_cons_left line 238
  19. def OAI.Prekopa.marginal line 246
  20. lemma OAI.Prekopa.Nice.section_integrable line 249
  21. lemma OAI.Prekopa.Nice.marginal line 262
  22. lemma OAI.Prekopa.integral_marginal line 295
  23. lemma OAI.Prekopa.fin line 305
  24. lemma OAI.Prekopa.infDist_combination line 340
  25. lemma OAI.Prekopa.sum_sq_combination line 357
  26. def OAI.Prekopa.approx line 367
  27. lemma OAI.Prekopa.approx_nice line 370
  28. lemma OAI.Prekopa.approx_interpolate line 385
  29. lemma OAI.Prekopa.approx_tendsto line 397
  30. lemma OAI.Prekopa.integral_approx_tendsto line 412
  31. lemma OAI.Prekopa.gauss_closed_logconcave line 425
  32. def OAI.Prekopa.normalConst line 448
  33. lemma OAI.Prekopa.normalConst_pos line 450
  34. lemma OAI.Prekopa.prod_pdf line 454
  35. lemma OAI.Prekopa.piGaussian_density line 467
  36. lemma OAI.Prekopa.piGaussian_real line 483
  37. lemma OAI.Prekopa.piGaussian_closed_logconcave line 493
  38. lemma OAI.Prekopa.linear_image_closed_logconcave line 519
  39. lemma OAI.Prekopa.stdGaussian_linear_image_closed_logconcave line 537
  40. lemma OAI.Prekopa.convex_closure_ae line 566
  41. lemma OAI.Prekopa.combination_closure line 581
  42. lemma OAI.Prekopa.piGaussian_convex_logconcave line 591
  43. lemma OAI.Prekopa.linear_image_convex_logconcave line 609
  44. lemma OAI.Prekopa.stdGaussian_linear_image_convex_logconcave line 631
  45. lemma OAI.Prekopa.weighted_approx_nice line 662
  46. lemma OAI.Prekopa.integral_weighted_approx_tendsto line 677
  47. lemma OAI.Prekopa.weighted_gauss_closed line 699
  48. lemma OAI.Prekopa.integral_weighted_gauss_tendsto line 732
  49. lemma OAI.Prekopa.bounded_weight_closed line 752
  50. lemma OAI.Prekopa.bounded_weight_compact_haar line 777
  51. lemma OAI.Prekopa.bounded_weight_convex_haar line 834