OAI/MathematicalPhysics/Boltzmann/Jets/ColdHotSourceDecomposition.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Exact separation of the hot source and the pure cold gain defect

  1. theorem OAI.BoltzmannNonuniqueness.HotRepresentative.cold_gain_defect_identity line 15
  2. theorem OAI.BoltzmannNonuniqueness.HotRepresentative.hot_cold_source_decomposition line 35