OAI/MathematicalPhysics/Boltzmann/Branching/RebuiltHotInitial.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A pointwise summable cold family over an almost-everywhere mild total state

  1. def OAI.BoltzmannNonuniqueness.WeightedLocal.rebuiltColdFamily line 20
  2. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.rebuiltColdFamily_properties line 24
  3. theorem OAI.BoltzmannNonuniqueness.PhaseEssSup.size_const_mul line 78
  4. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.rebuilt_hot_initial_ae line 89