OAI/MathematicalPhysics/Boltzmann/Collision/KernelInvariantPowers.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Monotonicity of the finite positive collision histories

  1. theorem OAI.BoltzmannNonuniqueness.KernelHistoryOrder.comp_mono line 20
  2. theorem OAI.BoltzmannNonuniqueness.KernelHistoryOrder.pow_mono line 28
  3. theorem OAI.BoltzmannNonuniqueness.KernelHistoryOrder.measure_comp_mono line 35
  4. theorem OAI.BoltzmannNonuniqueness.compProd_density_const line 61
  5. theorem OAI.BoltzmannNonuniqueness.kernel_pow_eq_on_invariant line 101