OAI/MathematicalPhysics/Boltzmann/Branching/CharacteristicCutoffGeometry.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Transport of collision kernels into characteristic coordinates

  1. def OAI.BoltzmannNonuniqueness.transportedKernel line 22
  2. instance OAI.BoltzmannNonuniqueness.transportedKernel_sFinite line 25
  3. theorem OAI.BoltzmannNonuniqueness.transportedKernel_comp line 30
  4. theorem OAI.BoltzmannNonuniqueness.relativeEntropy_eq_lintegral line 56
  5. theorem OAI.BoltzmannNonuniqueness.TorusFlight.scalar_entropy_lintegral_comp line 69
  6. def OAI.BoltzmannNonuniqueness.EuclideanFlight.centeredFlightChart line 95
  7. theorem OAI.BoltzmannNonuniqueness.EuclideanFlight.exists_characteristic_phase_cutoff line 103
  8. theorem OAI.BoltzmannNonuniqueness.EuclideanFlight.phase_displacement_bound line 164