OAI/MathematicalPhysics/Boltzmann/Branching/BoundedCollisionBlocks.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

Integrability of the finite cutoff source in Eulerian and characteristic coordinates

  1. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.bounded_cutoff_source_integrable line 27
  2. theorem OAI.BoltzmannNonuniqueness.cutoffPhysicalSource_eq line 53
  3. theorem OAI.BoltzmannNonuniqueness.cutoffPhysicalSource_measurable line 57
  4. theorem OAI.BoltzmannNonuniqueness.cutoffPhysicalSource_integrable line 66
  5. theorem OAI.BoltzmannNonuniqueness.cutoffCharacteristicSource_integrable line 76
  6. abbrev OAI.BoltzmannNonuniqueness.BoundedMeasurable.SupSpace line 108
  7. def OAI.BoltzmannNonuniqueness.BoundedMeasurable.measurableSet line 110
  8. theorem OAI.BoltzmannNonuniqueness.BoundedMeasurable.measurableSet_closed line 112
  9. abbrev OAI.BoltzmannNonuniqueness.BoundedMeasurable.Space line 118
  10. instance OAI.BoltzmannNonuniqueness.BoundedMeasurable.(instance at line 120) line 120
  11. instance OAI.BoltzmannNonuniqueness.BoundedMeasurable.(instance at line 122) line 122
  12. theorem OAI.BoltzmannNonuniqueness.BoundedMeasurable.measurable line 124
  13. def OAI.BoltzmannNonuniqueness.BoundedMeasurable.ofBounded line 126
  14. theorem OAI.BoltzmannNonuniqueness.BoundedMeasurable.ofBounded_apply line 129
  15. theorem OAI.BoltzmannNonuniqueness.BoundedMeasurable.dist_apply_le line 132
  16. theorem OAI.BoltzmannNonuniqueness.BoundedMeasurable.dist_le line 136
  17. def OAI.BoltzmannNonuniqueness.BoundedMeasurable.positiveBall line 144
  18. theorem OAI.BoltzmannNonuniqueness.BoundedMeasurable.positiveBall_closed line 146
  19. abbrev OAI.BoltzmannNonuniqueness.BoundedMeasurable.PositiveBall line 154
  20. instance OAI.BoltzmannNonuniqueness.BoundedMeasurable.(instance at line 156) line 156
  21. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.boundedMediumWordDensity line 176
  22. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.boundedMediumWordDensity_measurable line 185
  23. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.boundedMediumWordDensity_eq line 204
  24. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.mediumVelocityBox line 252
  25. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.mediumVelocityBox_measurable line 254
  26. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.boundedMediumEventKernel line 258
  27. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.boundedMediumEventKernel_sFinite line 262
  28. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.boundedMediumEventKernel_lintegral line 267
  29. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.boundedMediumEventKernel_pow_sFinite line 282
  30. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.boundedMediumWord_integral line 293
  31. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.boundedMediumBlockIntegrand line 349
  32. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.boundedMediumBlockMass line 356
  33. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.bounded_medium_word_integrand_bound line 361
  34. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.bounded_medium_word_integral_lower line 379
  35. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.boundedMediumEndpointKernel line 415
  36. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.boundedMediumEndpointKernel_isSFinite line 420
  37. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.boundedMediumEndpointKernel_lintegral line 430
  38. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.boundedMediumEndpointKernel_apply line 442
  39. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.boundedMediumBlockMass_endpoints line 452
  40. def OAI.BoltzmannNonuniqueness.regularizedRelativeEntropyDensity line 483
  41. theorem OAI.BoltzmannNonuniqueness.regularizedRelativeEntropyDensity_integrable line 486
  42. theorem OAI.BoltzmannNonuniqueness.bounded_mild_entropy_balance line 493
  43. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.bounded_finite_history_block_transfer line 599
  44. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.uniform_bounded_perturbed_block_growth line 655