OAI/Analysis/KLS/Convexity/PrekopaLeindler.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.AsymptoticStatistics.prekopaLeindler_1d_levelInclusion line 17
2. lemma OAI.AsymptoticStatistics.oneDim_brunn_minkowski_compact_le line 48
3. theorem OAI.AsymptoticStatistics.oneDim_brunn_minkowski_le line 125
4. theorem OAI.AsymptoticStatistics.prekopaLeindler_1d_levelMeasureBound line 267
5. theorem OAI.AsymptoticStatistics.lintegral_eq_lintegral_meas_lt_ennreal line 310
6. theorem OAI.AsymptoticStatistics.ennreal_geom_mean_le_arith_mean2_weighted line 390
7. theorem OAI.AsymptoticStatistics.prekopaLeindler_1d_arithBound line 436
8. theorem OAI.AsymptoticStatistics.prekopaLeindler_1d_essBdd line 526
9. theorem OAI.AsymptoticStatistics.prekopaLeindler_1d line 602
10. theorem OAI.AsymptoticStatistics.prekopaLeindler line 683