OAI/Probability/JammingConcavity/GaussianColeHopf.lean

GitHub source file

71 declarations, 0 contain sorry, 0 declared as axioms

Gaussian Cole Hopf.

  1. def OAI.MicroscopicJamming.RowAnalyticTerminal line 21
  2. def OAI.MicroscopicJamming.gaussianHeat line 27
  3. def OAI.MicroscopicJamming.gaussianRowOperator line 30
  4. def OAI.MicroscopicJamming.GaussianColeHopfStatement line 33
  5. def OAI.MicroscopicJamming.gaussianRowComposition line 50
  6. def OAI.MicroscopicJamming.gaussianStepTime line 54
  7. def OAI.MicroscopicJamming.GaussianStepBoundsStatement line 56
  8. def OAI.MicroscopicJamming.gaussianStepRemainder line 73
  9. def OAI.MicroscopicJamming.gaussianStepPath line 77
  10. def OAI.MicroscopicJamming.GaussianStepPathStatement line 80
  11. abbrev OAI.MicroscopicJamming.RowCylinder line 106
  12. def OAI.MicroscopicJamming.GaussianStepCompactnessStatement line 110
  13. def OAI.MicroscopicJamming.cloudUniform line 129
  14. abbrev OAI.MicroscopicJamming.MarkedCloud line 130
  15. def OAI.MicroscopicJamming.markedCloudLaw line 132
  16. def OAI.MicroscopicJamming.stableCloudWeight line 136
  17. def OAI.MicroscopicJamming.stableCloudSum line 141
  18. def OAI.MicroscopicJamming.StableCloudStatement line 144
  19. lemma OAI.MicroscopicJamming.iid_prefix_map line 168
  20. lemma OAI.MicroscopicJamming.iid_prefix_product line 175
  21. lemma OAI.MicroscopicJamming.poisson_one_pgf line 190
  22. lemma OAI.MicroscopicJamming.compound_poisson_product line 202
  23. def OAI.MicroscopicJamming.expNeg line 230
  24. lemma OAI.MicroscopicJamming.expNeg_nonneg line 232
  25. lemma OAI.MicroscopicJamming.expNeg_le_one line 233
  26. lemma OAI.MicroscopicJamming.expNeg_norm_le line 237
  27. lemma OAI.MicroscopicJamming.continuous_expNeg line 240
  28. lemma OAI.MicroscopicJamming.expNeg_zero line 250
  29. lemma OAI.MicroscopicJamming.expNeg_top line 251
  30. lemma OAI.MicroscopicJamming.expNeg_ofReal line 252
  31. lemma OAI.MicroscopicJamming.expNeg_eq_of_ne_top line 254
  32. lemma OAI.MicroscopicJamming.expNeg_add line 257
  33. lemma OAI.MicroscopicJamming.expNeg_sum line 261
  34. lemma OAI.MicroscopicJamming.integral_expNeg_tsum line 268
  35. lemma OAI.MicroscopicJamming.iid_prefix_product_varying line 288
  36. abbrev OAI.MicroscopicJamming.PoissonBin line 304
  37. def OAI.MicroscopicJamming.poissonBinLaw line 305
  38. def OAI.MicroscopicJamming.poissonSeriesLaw line 307
  39. def OAI.MicroscopicJamming.poissonBinSum line 309
  40. instance OAI.MicroscopicJamming.poissonBinLaw_probability line 312
  41. instance OAI.MicroscopicJamming.poissonSeriesLaw_probability line 315
  42. lemma OAI.MicroscopicJamming.measurable_poissonBinSum line 319
  43. lemma OAI.MicroscopicJamming.integrable_expNeg line 326
  44. lemma OAI.MicroscopicJamming.poissonBin_laplace line 332
  45. lemma OAI.MicroscopicJamming.poisson_series_laplace line 343
  46. lemma OAI.MicroscopicJamming.integral_exp_neg_zero line 373
  47. lemma OAI.MicroscopicJamming.stable_tail_iff line 378
  48. lemma OAI.MicroscopicJamming.stable_tail_measure line 386
  49. lemma OAI.MicroscopicJamming.stable_lintegral line 397
  50. lemma OAI.MicroscopicJamming.stable_integrable line 438
  51. lemma OAI.MicroscopicJamming.stable_integral line 448
  52. lemma OAI.MicroscopicJamming.unit_bins_union line 467
  53. lemma OAI.MicroscopicJamming.unit_bins_disjoint line 475
  54. lemma OAI.MicroscopicJamming.integral_unit_shift line 478
  55. lemma OAI.MicroscopicJamming.hasSum_integral_unit_shifts line 484
  56. def OAI.MicroscopicJamming.stableIntensity line 499
  57. lemma OAI.MicroscopicJamming.stableIntensity_nonneg line 502
  58. lemma OAI.MicroscopicJamming.stableIntensity_slice line 510
  59. lemma OAI.MicroscopicJamming.stableIntensity_integrable line 520
  60. lemma OAI.MicroscopicJamming.stableIntensity_integral line 541
  61. lemma OAI.MicroscopicJamming.stableIntensity_bins line 550
  62. instance OAI.MicroscopicJamming.cloudUniform_probability line 569
  63. instance OAI.MicroscopicJamming.markedCloudLaw_probability line 573
  64. lemma OAI.MicroscopicJamming.stableCloudSum_bins line 577
  65. lemma OAI.MicroscopicJamming.measurable_stableCloudSum line 591
  66. lemma OAI.MicroscopicJamming.cloud_laplace_extended line 599
  67. abbrev OAI.MicroscopicJamming.PointCloud line 650
  68. def OAI.MicroscopicJamming.pointCloudLaw line 652
  69. def OAI.MicroscopicJamming.pointCloudFunctional line 655
  70. def OAI.MicroscopicJamming.pointCloudTilt line 658
  71. def OAI.MicroscopicJamming.PointCloudMarkingStatement line 661