OAI/MathematicalPhysics/Boltzmann/Jets/TorusCharacteristic.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

Transfer of the actual cap sequence to the Euclidean fundamental cell

  1. def OAI.BoltzmannNonuniqueness.TorusKineticChart.cellVolume line 22
  2. def OAI.BoltzmannNonuniqueness.TorusKineticChart.chart line 25
  3. theorem OAI.BoltzmannNonuniqueness.TorusKineticChart.measurePreserving line 28
  4. theorem OAI.BoltzmannNonuniqueness.TorusKineticChart.density_comp line 33
  5. theorem OAI.BoltzmannNonuniqueness.TorusKineticChart.source_comp line 40
  6. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.CompactCapFamily.density_ui_cell line 56
  7. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.CompactCapFamily.source_ui_cell line 65
  8. theorem OAI.BoltzmannNonuniqueness.TorusPeriodicity.exists_lattice_difference line 93
  9. theorem OAI.BoltzmannNonuniqueness.TorusPeriodicity.spatial_difference line 107
  10. theorem OAI.BoltzmannNonuniqueness.TorusPeriodicity.density_eq_of_projection_eq line 117
  11. theorem OAI.BoltzmannNonuniqueness.TorusPeriodicity.density_descends line 130
  12. theorem OAI.BoltzmannNonuniqueness.TorusPeriodicity.source_descends line 139
  13. def OAI.BoltzmannNonuniqueness.TorusKineticChart.pairCellVolume line 165
  14. def OAI.BoltzmannNonuniqueness.TorusKineticChart.pairChart line 168
  15. theorem OAI.BoltzmannNonuniqueness.TorusKineticChart.pair_measurePreserving line 172
  16. theorem OAI.BoltzmannNonuniqueness.TorusKineticChart.pair_comp line 177
  17. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.CompactCapFamily.raw_pairs_ui_cell line 192
  18. def OAI.BoltzmannNonuniqueness.TorusKineticChart.liftDensity line 223
  19. def OAI.BoltzmannNonuniqueness.TorusKineticChart.liftPair line 226
  20. theorem OAI.BoltzmannNonuniqueness.TorusKineticChart.projection_measurable line 230
  21. theorem OAI.BoltzmannNonuniqueness.TorusKineticChart.liftDensity_measurable line 234
  22. theorem OAI.BoltzmannNonuniqueness.TorusKineticChart.liftPair_measurable line 239
  23. theorem OAI.BoltzmannNonuniqueness.TorusKineticChart.liftDensity_comp line 244
  24. theorem OAI.BoltzmannNonuniqueness.TorusKineticChart.liftPair_comp line 248
  25. theorem OAI.BoltzmannNonuniqueness.TorusKineticChart.weak_density_transfer line 253
  26. theorem OAI.BoltzmannNonuniqueness.TorusKineticChart.weak_pair_transfer line 263
  27. def OAI.BoltzmannNonuniqueness.TorusFlight.initialDensity line 291
  28. theorem OAI.BoltzmannNonuniqueness.TorusFlight.projection_flight line 294
  29. theorem OAI.BoltzmannNonuniqueness.TorusFlight.characteristic line 302