OAI/MathematicalPhysics/Boltzmann/Branching/ClippedColdTime.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Spatial covariance of clipped cold limits and dominated representatives

  1. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.clippedColdPicard_pull line 17
  2. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.clippedColdLimit_pull line 27
  3. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.normalizedFamily_reindex line 34
  4. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.rebuiltColdFamily_pull line 49
  5. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.rebuiltColdFamily_reindex line 57
  6. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.clippedColdPicard_time_clamp line 79
  7. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.clippedColdLimit_time_clamp line 91
  8. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.rebuiltColdFamily_time_clamp line 100
  9. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.mild_all_of_time_clamp line 110