OAI/MathematicalPhysics/Boltzmann/Jets/AnnularCharacteristicCutoff.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

One smooth cutoff and one physical clock for a whole short annular window

  1. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.exists_annular_characteristic_cutoff line 15