OAI/Probability/JammingConcavity/UniformPolynomialGrowth.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

Uniform Polynomial Growth.

  1. def OAI.MicroscopicJamming.Higher.UniformPolynomialGrowth line 28
  2. lemma OAI.MicroscopicJamming.Higher.UniformPolynomialGrowth.at line 31
  3. lemma OAI.MicroscopicJamming.Higher.PolynomialGrowth.uniform line 36
  4. lemma OAI.MicroscopicJamming.Higher.UniformPolynomialGrowth.comp line 41
  5. lemma OAI.MicroscopicJamming.Higher.UniformPolynomialGrowth.const line 47
  6. lemma OAI.MicroscopicJamming.Higher.UniformPolynomialGrowth.add line 50
  7. lemma OAI.MicroscopicJamming.Higher.UniformPolynomialGrowth.mul line 64
  8. lemma OAI.MicroscopicJamming.Higher.UniformPolynomialGrowth.const_mul line 76
  9. lemma OAI.MicroscopicJamming.Higher.UniformPolynomialGrowth.sub line 80
  10. lemma OAI.MicroscopicJamming.Higher.UniformPolynomialGrowth.pow line 85
  11. lemma OAI.MicroscopicJamming.Higher.UniformPolynomialGrowth.finset_sum line 92
  12. lemma OAI.MicroscopicJamming.Higher.affine_continuousAt line 111
  13. lemma OAI.MicroscopicJamming.Higher.heat_jointly_continuous line 143
  14. def OAI.MicroscopicJamming.Higher.normalizedHeatJet line 161
  15. lemma OAI.MicroscopicJamming.Higher.exp_heat_pos line 165
  16. lemma OAI.MicroscopicJamming.Higher.tilted_heat_polynomial line 172
  17. lemma OAI.MicroscopicJamming.Higher.heat_uniform_growth line 188
  18. lemma OAI.MicroscopicJamming.Higher.normalizedHeatJet_growth line 195
  19. lemma OAI.MicroscopicJamming.Higher.exp_smoothPolynomial line 203
  20. lemma OAI.MicroscopicJamming.Higher.normalizedHeatJet_smooth line 207
  21. lemma OAI.MicroscopicJamming.Higher.normalizedHeatJet_space line 218
  22. lemma OAI.MicroscopicJamming.Higher.normalizedHeatJet_time line 234
  23. lemma OAI.MicroscopicJamming.Higher.normalizedHeatJet_jointly_continuous line 247
  24. lemma OAI.MicroscopicJamming.Higher.normalizedHeatJet_iterated_growth line 255
  25. lemma OAI.MicroscopicJamming.Higher.normalizedHeatJet_smoothPolynomial line 287
  26. lemma OAI.MicroscopicJamming.Higher.gaussianRowOperator_deriv_normalized line 304
  27. lemma OAI.MicroscopicJamming.Higher.gaussianRowOperator_polynomial line 319
  28. lemma OAI.MicroscopicJamming.Higher.gaussianRowOperator_smoothPolynomial line 338
  29. lemma OAI.MicroscopicJamming.Higher.gaussianRowComposition_twice line 373
  30. lemma OAI.MicroscopicJamming.Higher.gaussianRowComposition_block_subcritical line 388
  31. lemma OAI.MicroscopicJamming.Higher.gaussianRowComposition_smoothPolynomial line 403
  32. def OAI.MicroscopicJamming.Higher.heatCumulant1 line 429
  33. def OAI.MicroscopicJamming.Higher.heatCumulant2 line 431
  34. def OAI.MicroscopicJamming.Higher.heatCumulant3 line 433
  35. def OAI.MicroscopicJamming.Higher.heatCumulant4 line 435
  36. def OAI.MicroscopicJamming.Higher.heatCumulant5 line 437
  37. lemma OAI.MicroscopicJamming.Higher.heatCumulant1_space line 440
  38. lemma OAI.MicroscopicJamming.Higher.heatCumulant2_space line 445
  39. lemma OAI.MicroscopicJamming.Higher.heatCumulant3_space line 451
  40. lemma OAI.MicroscopicJamming.Higher.heatCumulant4_space line 457
  41. lemma OAI.MicroscopicJamming.Higher.heatCumulant3_time line 464
  42. lemma OAI.MicroscopicJamming.Higher.gaussianRowOperator_cumulants line 482
  43. lemma OAI.MicroscopicJamming.Higher.gaussianRowOperator_third_equation line 515
  44. lemma OAI.MicroscopicJamming.Higher.gaussianRowOperator_third_continuous line 532
  45. lemma OAI.MicroscopicJamming.Higher.gaussianRowOperator_third_growth line 547