OAI/MathematicalPhysics/Boltzmann/Jets/TorusTransport.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

Free transport and its measure-preserving characteristic coordinates on the torus

  1. def OAI.BoltzmannNonuniqueness.TorusFlight.flight line 23
  2. theorem OAI.BoltzmannNonuniqueness.TorusFlight.continuous_flight line 25
  3. theorem OAI.BoltzmannNonuniqueness.TorusFlight.measurable_flight line 29
  4. theorem OAI.BoltzmannNonuniqueness.TorusFlight.flight_add line 32
  5. theorem OAI.BoltzmannNonuniqueness.TorusFlight.flight_zero line 40
  6. theorem OAI.BoltzmannNonuniqueness.TorusFlight.flight_neg line 46
  7. theorem OAI.BoltzmannNonuniqueness.TorusFlight.neg_flight line 49
  8. theorem OAI.BoltzmannNonuniqueness.TorusFlight.flight_measurePreserving line 52
  9. def OAI.BoltzmannNonuniqueness.TorusFlight.along line 67
  10. theorem OAI.BoltzmannNonuniqueness.TorusFlight.along_measurePreserving line 69
  11. theorem OAI.BoltzmannNonuniqueness.TorusFlight.back_measurePreserving line 75
  12. theorem OAI.BoltzmannNonuniqueness.TorusFlight.weak_along line 82
  13. def OAI.BoltzmannNonuniqueness.TorusFlight.continuousFlight line 110
  14. theorem OAI.BoltzmannNonuniqueness.TorusFlight.continuous_continuousFlight line 113
  15. theorem OAI.BoltzmannNonuniqueness.TorusFlight.tendsto_flight_L1 line 116
  16. def OAI.BoltzmannNonuniqueness.TorusFlight.flightEquiv line 154
  17. theorem OAI.BoltzmannNonuniqueness.TorusFlight.integral_flight line 162
  18. theorem OAI.BoltzmannNonuniqueness.Published.integral_timePrimitive line 170
  19. theorem OAI.BoltzmannNonuniqueness.TorusFlight.integral_along line 198
  20. theorem OAI.BoltzmannNonuniqueness.centered_characteristic_projection line 223
  21. theorem OAI.BoltzmannNonuniqueness.KineticTest.hasDerivAt_along line 236
  22. theorem OAI.BoltzmannNonuniqueness.MassTest.hasDerivAt_along line 254
  23. theorem OAI.BoltzmannNonuniqueness.time_shift_support line 285
  24. def OAI.BoltzmannNonuniqueness.KineticTest.timeShift line 293
  25. theorem OAI.BoltzmannNonuniqueness.KineticTest.timeShift_toFun line 306
  26. theorem OAI.BoltzmannNonuniqueness.KineticTest.timeShift_transportDerivative line 309
  27. def OAI.BoltzmannNonuniqueness.MassTest.timeShift line 322
  28. theorem OAI.BoltzmannNonuniqueness.MassTest.timeShift_toFun line 330
  29. theorem OAI.BoltzmannNonuniqueness.MassTest.timeShift_transportDerivative line 333
  30. theorem OAI.BoltzmannNonuniqueness.measurable_torusRepresentative line 362
  31. theorem OAI.BoltzmannNonuniqueness.measurable_kineticTestPoint line 371
  32. theorem OAI.BoltzmannNonuniqueness.KineticTest.measurable_toFun line 375
  33. theorem OAI.BoltzmannNonuniqueness.KineticTest.measurable_transportDerivative line 382
  34. theorem OAI.BoltzmannNonuniqueness.MassTest.measurable_toFun line 388
  35. theorem OAI.BoltzmannNonuniqueness.MassTest.measurable_transportDerivative line 397
  36. def OAI.BoltzmannNonuniqueness.fundamentalCube line 421
  37. theorem OAI.BoltzmannNonuniqueness.fundamentalCube_compact line 424
  38. theorem OAI.BoltzmannNonuniqueness.representative_mem_cube line 428
  39. theorem OAI.BoltzmannNonuniqueness.kinetic_lift_support line 434
  40. theorem OAI.BoltzmannNonuniqueness.kinetic_bounds_on_box line 444
  41. theorem OAI.BoltzmannNonuniqueness.velocity_fderiv_zero line 466
  42. theorem OAI.BoltzmannNonuniqueness.kinetic_derivative_zero line 472
  43. theorem OAI.BoltzmannNonuniqueness.KineticTest.bounded_on_time line 480
  44. theorem OAI.BoltzmannNonuniqueness.MassTest.bounded_on_time line 502
  45. theorem OAI.BoltzmannNonuniqueness.TorusFlight.strong_curve_flight line 542
  46. theorem OAI.BoltzmannNonuniqueness.KineticTest.contDiff_along line 583
  47. theorem OAI.BoltzmannNonuniqueness.MassTest.contDiff_along line 594
  48. theorem OAI.BoltzmannNonuniqueness.FiniteEntropyDatum.comp_flight line 618
  49. theorem OAI.BoltzmannNonuniqueness.TorusFlight.entropyMoment_integral_comp line 628