OAI/MathematicalPhysics/Boltzmann/Approximation/MildDensityAgreement.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Equality of strong time representatives implies equality of weak densities

  1. theorem OAI.BoltzmannNonuniqueness.kineticDensity_agreement line 12
  2. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.CapLocalLimit.density_eq_dormant line 26