OAI/MathematicalPhysics/Boltzmann/Compactness/LocalizedDampedBalance.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Localizing the physical normal-angle source above the cold spatial cutoff

  1. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.coldCharacteristicDomain line 23
  2. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.coldCharacteristicDomain_measurable line 27
  3. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.localizedNormalBeamKernel line 34
  4. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.localizedNormalBeamKernel_sFinite line 41
  5. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.localizedNormalCollision line 63
  6. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.localizedNormalCollision_sFinite line 69
  7. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.localizedNormalCollision_eq_restrict line 75
  8. def OAI.BoltzmannNonuniqueness.WeakTime.phaseWeight line 115
  9. def OAI.BoltzmannNonuniqueness.WeakTime.weightedPhaseSource line 117
  10. theorem OAI.BoltzmannNonuniqueness.WeakTime.phaseWeight_integrable line 120
  11. theorem OAI.BoltzmannNonuniqueness.WeakTime.weightedPhaseSource_finite line 127
  12. theorem OAI.BoltzmannNonuniqueness.WeakTime.ae_localized_measure_interval_balance line 136
  13. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.localizedNormalPhysicalEvent line 187
  14. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.localizedNormalPhysicalEvent_sFinite line 192
  15. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.boundedCollision_le_localized line 198
  16. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.boundedHistory_le_localized line 216
  17. theorem OAI.BoltzmannNonuniqueness.WeakTime.ae_localized_damped_measure_balance line 259