OAI/MathematicalPhysics/Boltzmann/Branching/AttenuationGap.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Stability of the nonnegative loss integrating factor

  1. theorem OAI.BoltzmannNonuniqueness.AttenuationLipschitz.exp_neg_difference_ordered line 17
  2. theorem OAI.BoltzmannNonuniqueness.AttenuationLipschitz.exp_neg_difference line 31
  3. theorem OAI.BoltzmannNonuniqueness.AttenuationLipschitz.attenuation_difference line 42
  4. theorem OAI.BoltzmannNonuniqueness.AttenuationLipschitz.attenuation_difference_le line 56
  5. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.one_sub_attenuation_le line 84
  6. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.abs_one_sub_attenuation_le line 95
  7. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.rateMultiplier_gap_le line 103