OAI/MathematicalPhysics/Boltzmann/Approximation/ColoredSourceDifferenceAE.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Collision integrand differences for a finite family in the sum norm

  1. theorem OAI.BoltzmannNonuniqueness.HotRepresentative.finite_integrand_abs_difference line 18
  2. theorem OAI.BoltzmannNonuniqueness.HotRepresentative.finite_gain_difference_sum line 66
  3. theorem OAI.BoltzmannNonuniqueness.HotRepresentative.finite_coldSource_difference_sum line 122
  4. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.finite_coldForcing_difference_ae line 201