OAI/MathematicalPhysics/HardSphere/GrandCanonical.lean

GitHub source file

93 declarations, 0 contain sorry, 0 declared as axioms

Grand-canonical hard-sphere probability and kinetic fluctuation preliminaries

This development proves microscopic law normalization, scattering and covariance algebra, exact centering, and compact and Gaussian-growth test estimates. The dynamics, backward Gaussian field, and finite-dimensional limit are specified, but their existence or convergence is not proved. The almost-everywhere deterministic flow and backward Gaussian field constructions, connected-history estimates, sharp cumulant bounds, discrepancy and centering transfer, and finite-dimensional convergence remain open here.

  1. abbrev OAI.HardSphereFluctuations.R3 line 23
  2. abbrev OAI.HardSphereFluctuations.Phase line 24
  3. abbrev OAI.HardSphereFluctuations.Test line 25
  4. abbrev OAI.HardSphereFluctuations.Density line 26
  5. abbrev OAI.HardSphereFluctuations.Sphere line 27
  6. def OAI.HardSphereFluctuations.sphereArea line 29
  7. def OAI.HardSphereFluctuations.collisionKernel line 31
  8. def OAI.HardSphereFluctuations.scatterLeft line 33
  9. def OAI.HardSphereFluctuations.scatterRight line 35
  10. def OAI.HardSphereFluctuations.pairDifference line 37
  11. def OAI.HardSphereFluctuations.latticePoint line 40
  12. def OAI.HardSphereFluctuations.bolNorm line 42
  13. def OAI.HardSphereFluctuations.spatialDerivative line 47
  14. def OAI.HardSphereFluctuations.boltzmannQ line 50
  15. structure OAI.HardSphereFluctuations.ClassicalBoltzmann line 57
  16. structure OAI.HardSphereFluctuations.KineticAssumption line 66
  17. def OAI.HardSphereFluctuations.collisionDrift line 78
  18. def OAI.HardSphereFluctuations.drift line 83
  19. abbrev OAI.HardSphereFluctuations.Collision line 86
  20. def OAI.HardSphereFluctuations.collisionBase line 88
  21. def OAI.HardSphereFluctuations.collisionWeight line 92
  22. def OAI.HardSphereFluctuations.collisionDifference line 96
  23. def OAI.HardSphereFluctuations.collisionCovariance line 99
  24. def OAI.HardSphereFluctuations.initialCovariance line 103
  25. abbrev OAI.HardSphereFluctuations.CompactTest line 105
  26. abbrev OAI.HardSphereFluctuations.TestCoordinates line 107
  27. def OAI.HardSphereFluctuations.testAtExponent line 109
  28. def OAI.HardSphereFluctuations.InTestSpace line 112
  29. def OAI.HardSphereFluctuations.SmallTest line 114
  30. abbrev OAI.HardSphereFluctuations.SmallTests line 116
  31. def OAI.HardSphereFluctuations.freeTransport line 118
  32. abbrev OAI.HardSphereFluctuations.Propagator line 120
  33. def OAI.HardSphereFluctuations.BoundedOnScales line 122
  34. structure OAI.HardSphereFluctuations.IsBackwardPropagator line 129
  35. abbrev OAI.HardSphereFluctuations.Configuration line 146
  36. abbrev OAI.HardSphereFluctuations.Microstate line 147
  37. def OAI.HardSphereFluctuations.admissible line 149
  38. def OAI.HardSphereFluctuations.particleIntensity line 152
  39. def OAI.HardSphereFluctuations.sectorLaw line 154
  40. def OAI.HardSphereFluctuations.grandCanonicalRaw line 162
  41. def OAI.HardSphereFluctuations.partitionFunction line 165
  42. def OAI.HardSphereFluctuations.grandCanonical line 168
  43. def OAI.HardSphereFluctuations.freeFlight line 171
  44. def OAI.HardSphereFluctuations.OneElasticImpact line 174
  45. def OAI.HardSphereFluctuations.IsRegularTrajectory line 185
  46. abbrev OAI.HardSphereFluctuations.Dynamics line 194
  47. def OAI.HardSphereFluctuations.IsHardSphereDynamics line 196
  48. def OAI.HardSphereFluctuations.empirical line 204
  49. def OAI.HardSphereFluctuations.microscopicFluctuation line 207
  50. def OAI.HardSphereFluctuations.initialMeasure line 212
  51. abbrev OAI.HardSphereFluctuations.SpaceTimeCollision line 215
  52. def OAI.HardSphereFluctuations.noiseMeasure line 217
  53. abbrev OAI.HardSphereFluctuations.L2 line 221
  54. def OAI.HardSphereFluctuations.toL2 line 223
  55. def OAI.HardSphereFluctuations.constantNoiseKernel line 227
  56. def OAI.HardSphereFluctuations.backwardNoiseKernel line 230
  57. structure OAI.HardSphereFluctuations.IsonormalPair line 233
  58. def OAI.HardSphereFluctuations.gaussianNoise line 243
  59. def OAI.HardSphereFluctuations.mildField line 248
  60. def OAI.HardSphereFluctuations.CenteredGaussianFamily line 254
  61. structure OAI.HardSphereFluctuations.IsFluctuationField line 259
  62. def OAI.HardSphereFluctuations.FiniteDimensionalLimit line 300
  63. structure OAI.HardSphereFluctuations.ProbabilitySpaceData line 310
  64. theorem OAI.HardSphereFluctuations.collisionKernel_nonnegative line 322
  65. theorem OAI.HardSphereFluctuations.scatter_momentum line 325
  66. theorem OAI.HardSphereFluctuations.scatter_energy line 330
  67. theorem OAI.HardSphereFluctuations.scatter_normal_reversed line 338
  68. theorem OAI.HardSphereFluctuations.scatterLeft_involutive line 344
  69. theorem OAI.HardSphereFluctuations.scatterRight_involutive line 351
  70. theorem OAI.HardSphereFluctuations.collisionKernel_prepost line 358
  71. theorem OAI.HardSphereFluctuations.pairDifference_linear line 364
  72. theorem OAI.HardSphereFluctuations.pairDifference_constant line 370
  73. theorem OAI.HardSphereFluctuations.pairDifference_momentum line 374
  74. theorem OAI.HardSphereFluctuations.pairDifference_energy line 380
  75. theorem OAI.HardSphereFluctuations.covariance_source_algebra line 386
  76. theorem OAI.HardSphereFluctuations.collisionWeight_nonnegative line 394
  77. theorem OAI.HardSphereFluctuations.collisionCovariance_symmetric line 400
  78. theorem OAI.HardSphereFluctuations.collisionCovariance_nonnegative line 405
  79. theorem OAI.HardSphereFluctuations.initialCovariance_symmetric line 414
  80. theorem OAI.HardSphereFluctuations.initialCovariance_nonnegative line 419
  81. theorem OAI.HardSphereFluctuations.sqrt_particleIntensity line 427
  82. theorem OAI.HardSphereFluctuations.microscopicFluctuation_integral_zero line 431
  83. theorem OAI.HardSphereFluctuations.toL2_ae line 440
  84. theorem OAI.HardSphereFluctuations.product_density_lintegral line 449
  85. theorem OAI.HardSphereFluctuations.sector_mass_le line 468
  86. theorem OAI.HardSphereFluctuations.sector_zero_mass line 487
  87. theorem OAI.HardSphereFluctuations.partitionFunction_eq_tsum line 492
  88. theorem OAI.HardSphereFluctuations.one_le_partitionFunction line 502
  89. theorem OAI.HardSphereFluctuations.partitionFunction_le_exp line 506
  90. theorem OAI.HardSphereFluctuations.grandCanonical_isProbability line 525
  91. theorem OAI.HardSphereFluctuations.compactTest_small line 540
  92. theorem OAI.HardSphereFluctuations.testAtExponent_bound line 550
  93. theorem OAI.HardSphereFluctuations.pairDifference_gaussian_bound line 563