OAI/MathematicalPhysics/Boltzmann/Compactness/LocalizedHotMassGrowth.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Converting finite angular blocks to growth of a dominated hot measure

  1. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.localizedHistoryBlockMass_eq_measure line 19
  2. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.localized_history_mass_growth line 36
  3. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.localizedNormalBeamKernel_independent line 72
  4. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.localizedHistoryBlockMass_independent line 99
  5. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.localized_hot_mass_growth line 126