OAI/MathematicalPhysics/Boltzmann/Collision/KernelInvariantOrder.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Finite sums commute with applying a kernel to a measure

  1. theorem OAI.BoltzmannNonuniqueness.kernel_finset_comp_measure line 15
  2. theorem OAI.BoltzmannNonuniqueness.kernel_pow_le_on_invariant line 42