OAI/Analysis/KLS/Spectral/BrascampLiebMoments.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.LeanBlast.KLS.boundedKernel_bound line 20
  2. theorem OAI.LeanBlast.KLS.boundedKernel_integrable line 28
  3. theorem OAI.LeanBlast.KLS.boundedKernel_hasDerivAt_integral line 39
  4. def OAI.LeanBlast.KLS.blWeight line 64
  5. def OAI.LeanBlast.KLS.blWeightDeriv line 66
  6. def OAI.LeanBlast.KLS.blWeightSecond line 68
  7. theorem OAI.LeanBlast.KLS.continuous_blWeight line 70
  8. theorem OAI.LeanBlast.KLS.continuous_blWeightDeriv line 75
  9. theorem OAI.LeanBlast.KLS.continuous_blWeightSecond line 80
  10. theorem OAI.LeanBlast.KLS.hasDerivAt_blWeight line 85
  11. theorem OAI.LeanBlast.KLS.hasDerivAt_blWeightDeriv line 92
  12. def OAI.LeanBlast.KLS.blMoment line 104
  13. def OAI.LeanBlast.KLS.blMomentDeriv line 105
  14. def OAI.LeanBlast.KLS.blMomentSecond line 106
  15. def OAI.LeanBlast.KLS.blLogMoment line 107
  16. theorem OAI.LeanBlast.KLS.blMoment_zero line 109
  17. theorem OAI.LeanBlast.KLS.blMomentDeriv_zero line 113
  18. theorem OAI.LeanBlast.KLS.blMomentSecond_zero line 117
  19. theorem OAI.LeanBlast.KLS.hasDerivAt_blMoment line 125
  20. theorem OAI.LeanBlast.KLS.hasDerivAt_blMomentDeriv line 132
  21. theorem OAI.LeanBlast.KLS.blMoment_pos line 139
  22. theorem OAI.LeanBlast.KLS.hasDerivAt_blLogMoment line 144
  23. theorem OAI.LeanBlast.KLS.hasDerivAt_deriv_blLogMoment_zero line 151
  24. theorem OAI.LeanBlast.KLS.variance_le_integral_of_concave_blLogMoment line 173