OAI/MathematicalPhysics/Boltzmann/Approximation/CappedDensitySequence.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

A common velocity moment for the actual capped torus densities

  1. def OAI.BoltzmannNonuniqueness.JetCopyDatum.momentBase line 24
  2. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.momentBase_nonneg line 27
  3. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.capped_torus_moment line 32
  4. def OAI.BoltzmannNonuniqueness.JetCopyDatum.torusPhysical line 78
  5. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.torusPhysical_measurable line 82
  6. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.torusPhysical_nonneg line 95
  7. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.capped_spacetime_moment line 99
  8. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.capped_torus_outer_bound line 144
  9. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.capped_spacetime_outer_bound line 206
  10. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.capped_family_pairs_uniformIntegrable line 258
  11. structure OAI.BoltzmannNonuniqueness.JetCopyDatum.CapApproximation line 310
  12. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.cap_family_pairs_uniformIntegrable line 322
  13. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.exists_integrable_cap_family line 349
  14. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.capped_family_density_uniformIntegrable line 391
  15. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.cap_family_density_uniformIntegrable line 443