OAI/MathematicalPhysics/Boltzmann/Approximation/MildRenormalizedBalance.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

The canonical integral paths agree with every-time physical traces

  1. theorem OAI.BoltzmannNonuniqueness.MildCollisionSolution.evolution_along_eq_path line 23
  2. theorem OAI.BoltzmannNonuniqueness.MildCollisionSolution.positiveEvolution_along_eq_path line 31
  3. theorem OAI.BoltzmannNonuniqueness.MildCollisionSolution.positiveEvolution_along_eq_path_spacetime line 40
  4. theorem OAI.BoltzmannNonuniqueness.MildCollisionSolution.weak_kinetic_trace line 67
  5. theorem OAI.BoltzmannNonuniqueness.MildCollisionSolution.source_mass_zero line 116
  6. theorem OAI.BoltzmannNonuniqueness.MildCollisionSolution.characteristicSource_mass_zero line 134
  7. theorem OAI.BoltzmannNonuniqueness.MildCollisionSolution.mass_conservation line 140
  8. theorem OAI.BoltzmannNonuniqueness.Published.timePrimitive_congr line 177
  9. theorem OAI.BoltzmannNonuniqueness.MildCollisionSolution.positiveDensity_source_eq_ae line 196
  10. theorem OAI.BoltzmannNonuniqueness.MildCollisionSolution.positiveEvolution_characteristic line 204
  11. theorem OAI.BoltzmannNonuniqueness.MildCollisionSolution.positiveEvolution_along_collision_eq_source line 256
  12. theorem OAI.BoltzmannNonuniqueness.MildCollisionSolution.renormalizedIntegrand_along_eq line 267
  13. theorem OAI.BoltzmannNonuniqueness.MildCollisionSolution.positiveEvolution_spacetime_integrable line 301
  14. theorem OAI.BoltzmannNonuniqueness.MildCollisionSolution.positiveEvolution_collision_integrable line 308
  15. theorem OAI.BoltzmannNonuniqueness.MildCollisionSolution.renormalized_integrable line 319
  16. theorem OAI.BoltzmannNonuniqueness.MildCollisionSolution.renormalized_balance line 348
  17. theorem OAI.BoltzmannNonuniqueness.MildCollisionSolution.renormalized_equation_of_terminal_zero line 394