OAI/MathematicalPhysics/Boltzmann/Branching/ClippedColdFiniteLimit.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Bounded positive cold iteration without a pointwise total fixed point

  1. def OAI.BoltzmannNonuniqueness.WeightedLocal.clippedColdPicard line 18
  2. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.clippedCold_properties line 24
  3. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.clippedCold_monotone line 53
  4. def OAI.BoltzmannNonuniqueness.WeightedLocal.clippedColdLimit line 105
  5. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.clippedCold_solution line 109
  6. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.clippedCold_finite_picard line 173
  7. def OAI.BoltzmannNonuniqueness.WeightedLocal.ColdMildAE line 254
  8. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.clippedCold_mildAE line 259
  9. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.clippedCold_envelope line 315
  10. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.clippedCold_finite_limit line 367