OAI/MathematicalPhysics/Boltzmann/Collision/KernelConjugacy.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Iteration commutes with an exact measurable change of coordinates

  1. theorem OAI.BoltzmannNonuniqueness.kernel_eq_transport_of_map line 16
  2. theorem OAI.BoltzmannNonuniqueness.transportedKernel_map line 26
  3. theorem OAI.BoltzmannNonuniqueness.kernel_pow_map line 34