OAI/MathematicalPhysics/Boltzmann/Approximation/MildRenormalization.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

A strongly continuous representative of the constructed local mild solution

  1. def OAI.BoltzmannNonuniqueness.MildCollisionSolution.source line 23
  2. def OAI.BoltzmannNonuniqueness.MildCollisionSolution.characteristicSource line 26
  3. def OAI.BoltzmannNonuniqueness.MildCollisionSolution.evolution line 29
  4. theorem OAI.BoltzmannNonuniqueness.MildCollisionSolution.source_measurable line 34
  5. theorem OAI.BoltzmannNonuniqueness.MildCollisionSolution.characteristicSource_measurable line 38
  6. theorem OAI.BoltzmannNonuniqueness.MildCollisionSolution.characteristicSource_integrable line 43
  7. theorem OAI.BoltzmannNonuniqueness.MildCollisionSolution.evolution_eq_ae line 55
  8. theorem OAI.BoltzmannNonuniqueness.MildCollisionSolution.evolution_strong_continuity line 65
  9. theorem OAI.BoltzmannNonuniqueness.MildCollisionSolution.evolution_initial line 72
  10. theorem OAI.BoltzmannNonuniqueness.continuous_path_nonnegative_of_ae line 95
  11. theorem OAI.BoltzmannNonuniqueness.MildCollisionSolution.nonnegative_integral_paths line 111
  12. theorem OAI.BoltzmannNonuniqueness.MildCollisionSolution.renormalized_integral_paths line 135
  13. theorem OAI.BoltzmannNonuniqueness.MildCollisionSolution.renormalized_tested_paths line 178
  14. theorem OAI.BoltzmannNonuniqueness.tested_absolutelyContinuous_path line 230
  15. theorem OAI.BoltzmannNonuniqueness.MildCollisionSolution.mass_tested_paths line 249