OAI/MathematicalPhysics/Boltzmann/Branching/CellLocalizedSource.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The finite spacetime measure of the fundamental cell

  1. def OAI.BoltzmannNonuniqueness.TorusKineticChart.baseVolume line 18
  2. instance OAI.BoltzmannNonuniqueness.TorusKineticChart.(instance at line 21) line 21
  3. theorem OAI.BoltzmannNonuniqueness.TorusKineticChart.baseVolume_le line 29
  4. theorem OAI.BoltzmannNonuniqueness.TorusKineticChart.cellVolume_eq_base line 32
  5. theorem OAI.BoltzmannNonuniqueness.TorusKineticChart.pairCellVolume_eq_base line 34
  6. def OAI.BoltzmannNonuniqueness.TorusKineticChart.region line 54
  7. theorem OAI.BoltzmannNonuniqueness.TorusKineticChart.measurableSet_region line 56
  8. theorem OAI.BoltzmannNonuniqueness.TorusKineticChart.cellVolume_eq line 59
  9. theorem OAI.BoltzmannNonuniqueness.TorusKineticChart.localizedSource_eq line 67
  10. theorem OAI.BoltzmannNonuniqueness.TorusKineticChart.uniformIntegrable_add line 83
  11. theorem OAI.BoltzmannNonuniqueness.TorusKineticChart.localizedSource_uniformIntegrable line 92
  12. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.CompactCapFamily.localized_source_ui line 120