OAI/Analysis/KLS/Convexity/LogConcavity.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.LeanBlast.KLS.IsLogConcaveFunction line 15
  2. theorem OAI.LeanBlast.KLS.IsLogConcaveDensity.isLogConcaveFunction line 19
  3. theorem OAI.LeanBlast.KLS.IsLogConcaveFunction.rpow_le line 23
  4. theorem OAI.LeanBlast.KLS.IsLogConcaveFunction.ennreal_rpow_le line 42
  5. theorem OAI.LeanBlast.KLS.isLogConcaveFunction_of_rpow_le line 51
  6. theorem OAI.LeanBlast.KLS.isLogConcaveFunction_of_ennreal line 80
  7. theorem OAI.LeanBlast.KLS.IsLogConcaveFunction.mul_exp line 90
  8. theorem OAI.LeanBlast.KLS.IsLogConcaveFunction.exp_mul line 101
  9. theorem OAI.LeanBlast.KLS.IsLogConcaveFunction.const_mul line 105
  10. theorem OAI.LeanBlast.KLS.IsLogConcaveFunction.div_const line 110
  11. theorem OAI.LeanBlast.KLS.IsLogConcaveFunction.mul line 114
  12. theorem OAI.LeanBlast.KLS.IsLogConcaveFunction.comp_linearMap line 125