OAI/Analysis/KLS/Spectral/BrascampLieb.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LeanBlast.KLS.exp_neg_blPerturbation line 15
2. theorem OAI.LeanBlast.KLS.blMoment_potentialMeasure line 23
3. theorem OAI.LeanBlast.KLS.concaveOn_blLogMoment_of_convex line 29
4. theorem OAI.LeanBlast.KLS.brascamp_lieb line 55
5. theorem OAI.LeanBlast.KLS.brascamp_lieb_normalized line 96