OAI/Probability/JammingConcavity/LogHeatCalculus.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Log Heat Calculus.

  1. lemma OAI.MicroscopicJamming.log_heat_calculus line 26
  2. lemma OAI.MicroscopicJamming.gaussianHeat_twice_calculus line 54
  3. lemma OAI.MicroscopicJamming.gaussianHeat_zero line 78
  4. lemma OAI.MicroscopicJamming.gaussianRowOperator_zero line 81
  5. lemma OAI.MicroscopicJamming.gaussianRowOperator_calculus line 87
  6. theorem OAI.MicroscopicJamming.gaussian_cole_hopf line 120
  7. def OAI.MicroscopicJamming.GaussianCurvatureStatement line 130
  8. lemma OAI.MicroscopicJamming.integral_four_linear line 143
  9. lemma OAI.MicroscopicJamming.integral_three_linear line 154
  10. lemma OAI.MicroscopicJamming.weighted_covariance_nonpos line 162
  11. lemma OAI.MicroscopicJamming.weighted_covariance_upper line 197
  12. lemma OAI.MicroscopicJamming.weighted_variance_nonneg line 214
  13. lemma OAI.MicroscopicJamming.gaussian_weighted_poly_integrable line 240
  14. structure OAI.MicroscopicJamming.GaussianRowMoments line 252
  15. lemma OAI.MicroscopicJamming.gaussianRowMoments line 261
  16. lemma OAI.MicroscopicJamming.row_gaussian_stein line 308
  17. lemma OAI.MicroscopicJamming.gaussianRowOperator_second_exp line 359
  18. lemma OAI.MicroscopicJamming.gaussianRowOperator_second_moments line 385
  19. lemma OAI.MicroscopicJamming.row_curvature_algebra line 417
  20. lemma OAI.MicroscopicJamming.row_slope_antitone line 457
  21. lemma OAI.MicroscopicJamming.gaussianRowOperator_second_zero line 472
  22. lemma OAI.MicroscopicJamming.gaussianRowOperator_curvature line 484
  23. theorem OAI.MicroscopicJamming.gaussian_curvature line 531