OAI/Probability/JammingConcavity/PolynomialHeat.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

Polynomial Heat.

  1. def OAI.MicroscopicJamming.Higher.PolynomialGrowth line 28
  2. lemma OAI.MicroscopicJamming.Higher.PolynomialGrowth.of_bound line 31
  3. lemma OAI.MicroscopicJamming.Higher.PolynomialGrowth.of_quadratic line 35
  4. lemma OAI.MicroscopicJamming.Higher.PolynomialGrowth.const line 40
  5. lemma OAI.MicroscopicJamming.Higher.PolynomialGrowth.add line 43
  6. lemma OAI.MicroscopicJamming.Higher.PolynomialGrowth.mul line 56
  7. lemma OAI.MicroscopicJamming.Higher.PolynomialGrowth.finset_sum line 67
  8. lemma OAI.MicroscopicJamming.Higher.affine_integrable line 75
  9. lemma OAI.MicroscopicJamming.Higher.affine_mul_integrable line 89
  10. lemma OAI.MicroscopicJamming.Higher.curve_derivative line 104
  11. lemma OAI.MicroscopicJamming.Higher.space_derivative line 162
  12. lemma OAI.MicroscopicJamming.Higher.time_derivative line 174
  13. lemma OAI.MicroscopicJamming.Higher.PolynomialGrowth.id line 220
  14. lemma OAI.MicroscopicJamming.Higher.PolynomialGrowth.pow line 223
  15. lemma OAI.MicroscopicJamming.Higher.PolynomialGrowth.affine line 229
  16. lemma OAI.MicroscopicJamming.Higher.weighted_poly_integrable line 239
  17. lemma OAI.MicroscopicJamming.Higher.tilted_even_stein line 249
  18. lemma OAI.MicroscopicJamming.Higher.tilted_slope_bound line 284
  19. lemma OAI.MicroscopicJamming.Higher.tilted_even_recurrence line 296
  20. lemma OAI.MicroscopicJamming.Higher.tilted_even_moment_bound line 352
  21. lemma OAI.MicroscopicJamming.Higher.one_abs_pow_le_even line 402
  22. lemma OAI.MicroscopicJamming.Higher.tilted_polynomial_bound line 417
  23. structure OAI.MicroscopicJamming.Higher.SmoothPolynomial line 484
  24. lemma OAI.MicroscopicJamming.Higher.SmoothPolynomial.differentiable line 488
  25. lemma OAI.MicroscopicJamming.Higher.SmoothPolynomial.continuous line 492
  26. lemma OAI.MicroscopicJamming.Higher.SmoothPolynomial.derivative line 495
  27. lemma OAI.MicroscopicJamming.Higher.SmoothPolynomial.const_mul line 501
  28. lemma OAI.MicroscopicJamming.Higher.SmoothPolynomial.exp line 510
  29. lemma OAI.MicroscopicJamming.Higher.row_terminal_smoothPolynomial line 540
  30. lemma OAI.MicroscopicJamming.Higher.heat_iterated_derivative line 549
  31. lemma OAI.MicroscopicJamming.Higher.heat_smooth line 560
  32. lemma OAI.MicroscopicJamming.Higher.heat_jet_time_derivative line 570
  33. lemma OAI.MicroscopicJamming.Higher.SmoothPolynomial.const line 589
  34. lemma OAI.MicroscopicJamming.Higher.SmoothPolynomial.add line 596
  35. lemma OAI.MicroscopicJamming.Higher.SmoothPolynomial.mul line 607
  36. lemma OAI.MicroscopicJamming.Higher.exp_jet_factor line 622