OAI/Analysis/KLS/Convexity/PrekopaReal.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LeanBlast.KLS.prekopaLeindler_integral line 11
2. theorem OAI.LeanBlast.KLS.concaveOn_log_integral line 33
3. theorem OAI.LeanBlast.KLS.concaveOn_log_integral_exp_neg line 64