OAI/Geometry/LatticeCovering/LogConcavity.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SingleLatticeCovering.Prekopa.integral_RV_zero line 16
  2. lemma OAI.SingleLatticeCovering.Prekopa.cons_weighted line 19
  3. theorem OAI.SingleLatticeCovering.Prekopa.gaussian_dominated_integral line 27
  4. lemma OAI.SingleLatticeCovering.Prekopa.sum_sq_le_norm_sq line 66
  5. def OAI.SingleLatticeCovering.Prekopa.softIndicator line 76
  6. lemma OAI.SingleLatticeCovering.Prekopa.softIndicator_positive line 79
  7. lemma OAI.SingleLatticeCovering.Prekopa.continuous_softIndicator line 82
  8. lemma OAI.SingleLatticeCovering.Prekopa.softIndicator_gaussianBound line 87
  9. lemma OAI.SingleLatticeCovering.Prekopa.infDist_weighted line 112
  10. lemma OAI.SingleLatticeCovering.Prekopa.softIndicator_weighted line 126
  11. lemma OAI.SingleLatticeCovering.Prekopa.softIndicator_tendsto line 148
  12. lemma OAI.SingleLatticeCovering.Prekopa.softIndicator_antitone line 168
  13. lemma OAI.SingleLatticeCovering.Prekopa.softIndicator_integral_tendsto line 174
  14. theorem OAI.SingleLatticeCovering.Prekopa.compact_volume line 190
  15. theorem OAI.SingleLatticeCovering.Prekopa.logConcave_section_volume line 233
  16. lemma OAI.SingleLatticeCovering.Prekopa.LogConcave.const_mul line 243
  17. theorem OAI.SingleLatticeCovering.Prekopa.logConcave_canonical_density line 256
  18. def OAI.SingleLatticeCovering.Prekopa.ScalarLogConcave line 269
  19. def OAI.SingleLatticeCovering.Prekopa.linearCap line 273
  20. lemma OAI.SingleLatticeCovering.Prekopa.linearCap_compact line 276
  21. theorem OAI.SingleLatticeCovering.Prekopa.scalarLogConcave_cap_volume line 280
  22. lemma OAI.SingleLatticeCovering.Prekopa.ScalarLogConcave.const_mul line 292
  23. lemma OAI.SingleLatticeCovering.Prekopa.ScalarLogConcave.log_interpolation line 303
  24. theorem OAI.SingleLatticeCovering.Prekopa.ScalarLogConcave.exponential_tail line 314
  25. lemma OAI.SingleLatticeCovering.Prekopa.right_derivative_nonpos_of_max line 369
  26. theorem OAI.SingleLatticeCovering.Prekopa.ScalarLogConcave.log_bound_at_weighted_mode line 379
  27. def OAI.SingleLatticeCovering.Prekopa.shellRate line 414
  28. theorem OAI.SingleLatticeCovering.Prekopa.ScalarLogConcave.weighted_mode_envelope line 418
  29. lemma OAI.SingleLatticeCovering.Prekopa.shellRate_ge_sqrt_sq line 445
  30. lemma OAI.SingleLatticeCovering.Prekopa.shellRate_ge_sq_div_nine line 451
  31. lemma OAI.SingleLatticeCovering.Prekopa.shellRate_support line 464
  32. lemma OAI.SingleLatticeCovering.Prekopa.shellRate_upper_tail line 473
  33. lemma OAI.SingleLatticeCovering.Prekopa.shellRate_lower_tail line 487
  34. lemma OAI.SingleLatticeCovering.Prekopa.integral_exp_shift_Ioi line 510
  35. lemma OAI.SingleLatticeCovering.Prekopa.integral_exp_shift_Iic line 519
  36. lemma OAI.SingleLatticeCovering.Prekopa.integrableOn_exp_shift_Ioi line 528
  37. lemma OAI.SingleLatticeCovering.Prekopa.integrableOn_exp_shift_Iic line 535
  38. lemma OAI.SingleLatticeCovering.Prekopa.ScalarLogConcave.upper_shell_envelope line 542
  39. lemma OAI.SingleLatticeCovering.Prekopa.ScalarLogConcave.lower_shell_envelope line 560
  40. lemma OAI.SingleLatticeCovering.Prekopa.ScalarLogConcave.upper_shell_integral line 577
  41. lemma OAI.SingleLatticeCovering.Prekopa.ScalarLogConcave.lower_shell_integral line 597
  42. lemma OAI.SingleLatticeCovering.Prekopa.radial_integral_lower line 620
  43. theorem OAI.SingleLatticeCovering.Prekopa.ScalarLogConcave.shell_integral_bound line 644
  44. lemma OAI.SingleLatticeCovering.Prekopa.exists_weighted_mode line 669