OAI/MathematicalPhysics/Boltzmann/Jets/TorusChart.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

A centered fundamental cube for the periodic spatial variable

  1. def OAI.BoltzmannNonuniqueness.TorusChart.interval line 14
  2. def OAI.BoltzmannNonuniqueness.TorusChart.cube line 16
  3. def OAI.BoltzmannNonuniqueness.TorusChart.coordinate line 18
  4. def OAI.BoltzmannNonuniqueness.TorusChart.representative line 21
  5. theorem OAI.BoltzmannNonuniqueness.TorusChart.coordinate_measurePreserving line 23
  6. theorem OAI.BoltzmannNonuniqueness.TorusChart.measurableSet_cube line 33
  7. theorem OAI.BoltzmannNonuniqueness.TorusChart.representative_measurePreserving line 39
  8. theorem OAI.BoltzmannNonuniqueness.TorusChart.representative_mem line 54
  9. theorem OAI.BoltzmannNonuniqueness.TorusChart.projection_representative line 63
  10. theorem OAI.BoltzmannNonuniqueness.TorusChart.representative_projection line 67
  11. def OAI.BoltzmannNonuniqueness.TorusChart.phaseRepresentative line 75
  12. theorem OAI.BoltzmannNonuniqueness.TorusChart.phase_measurePreserving line 77