OAI/MathematicalPhysics/Boltzmann/Compactness/PeriodicStrongAverages.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

A real-valued joint entropy budget on each finite right interval

  1. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalWeakLimit.entropy_path_integrable line 32
  2. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalWeakLimit.entropyMarginal_ae_eq line 41
  3. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.real_joint_interval_budget line 47
  4. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.velocity_average_strong line 97
  5. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.bounded_kernel_strong line 148
  6. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.linear_kernel_strong line 185
  7. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.frequency_strong line 250
  8. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.sharp_joint_entropy_dissipation line 305
  9. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.physicalCharacteristicFrequency line 347
  10. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.physicalCharacteristicPrimitive line 350
  11. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.physicalCharacteristicSurvival line 353
  12. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.physicalCharacteristicFrequency_measurable line 356
  13. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.physicalCharacteristicFrequency_nonneg line 361
  14. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.physicalCharacteristicFrequency_integrable line 365
  15. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.characteristic_frequency_strong line 375
  16. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.characteristic_frequency_integrable line 389
  17. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.characteristic_primitive_strong line 413
  18. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.characteristic_survival_strong line 428
  19. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.velocity_fiber_moments line 462
  20. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.loss_le_frequency line 476
  21. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.frequency_bounded line 487
  22. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.frequency_path_integrable line 514
  23. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.characteristicGain line 541
  24. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.characteristicGain_measurable line 544
  25. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.gain_path_integrable line 549
  26. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.positive_physical_survival line 560
  27. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.characteristicLossDefect line 640
  28. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.characteristicLossDefect_measurable line 645
  29. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.physical_loss_eq line 651
  30. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.characteristicLossDefect_eq line 658
  31. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.characteristicLossDefect_nonneg line 667
  32. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.lossDefect_path_integrable line 672
  33. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.dampedPath line 708
  34. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.dampedPath_eq line 712
  35. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.dampedPath_initial line 716
  36. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.dampedPath_absolutelyContinuous line 719
  37. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.dampedPath_physical_derivative line 724
  38. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.positive_comparison line 765
  39. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.survivingInitial line 829
  40. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.surviving_initial_strong line 832
  41. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.pair_product_average_strong line 880
  42. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.pair_compact_average_strong line 930
  43. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.pair_compact_kernel_strong line 998
  44. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.linear_velocity_average_strong line 1042
  45. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.conserved_linear_moment_ae line 1083
  46. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.conserved_linear_moment_ae_nonneg line 1142
  47. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.mass_conservation_ae line 1158
  48. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.momentum_conservation_ae line 1173
  49. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.smoothed_angular_average_strong line 1206
  50. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.two_time_survival_strong line 1241
  51. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.angular_pair_average_strong line 1274