OAI/MathematicalPhysics/Boltzmann/Branching/SpacetimeFourierCoordinates.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Hilbert coordinates for the evolution transport Fourier transform

  1. abbrev OAI.BoltzmannNonuniqueness.Published.FourierSpace line 12
  2. def OAI.BoltzmannNonuniqueness.Published.spacetimeHilbertEquiv line 14
  3. theorem OAI.BoltzmannNonuniqueness.Published.spacetimeHilbert_measurePreserving line 16
  4. def OAI.BoltzmannNonuniqueness.Published.characteristicDirection line 20
  5. theorem OAI.BoltzmannNonuniqueness.Published.characteristicFrequency line 22
  6. theorem OAI.BoltzmannNonuniqueness.Published.spacetimeHilbert_translation line 26