OAI/MathematicalPhysics/Boltzmann/Compactness/PeriodicMomentEntropy.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

Integrable undamped sources of the actual periodic cutoff solutions

  1. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.collision line 20
  2. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.characteristicSource line 23
  3. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.collision_eq line 26
  4. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.collision_measurable line 32
  5. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.collision_support line 35
  6. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.collision_bounded line 39
  7. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.weighted_collision_integrable line 56
  8. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.characteristicSource_measurable line 85
  9. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.weighted_characteristic_integrable line 89
  10. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.eulerianProfile_eq line 97
  11. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.weighted_density_integrable line 122
  12. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.weighted_collision_zero line 141
  13. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.weighted_characteristic_zero line 159
  14. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.moment_conservation line 168
  15. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.kinetic_collision line 212
  16. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.log_collision_integrable line 219
  17. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.entropy_production_bound line 241
  18. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.endpoint_entropy_integrable line 277
  19. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.integrated_entropy_balance line 286
  20. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.endpoint_entropy_tendsto line 343
  21. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.entropy_inequality line 352
  22. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.relativeEntropy_le line 374
  23. def OAI.BoltzmannNonuniqueness.compactKernelMass line 394
  24. theorem OAI.BoltzmannNonuniqueness.compactKernelMass_eq line 397
  25. theorem OAI.BoltzmannNonuniqueness.compactKernelMass_nonneg line 401
  26. theorem OAI.BoltzmannNonuniqueness.compactKernelMass_le line 406
  27. theorem OAI.BoltzmannNonuniqueness.linear_over_quadratic_bound line 423
  28. theorem OAI.BoltzmannNonuniqueness.hardSphere_kernel_condition line 436
  29. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.kineticProfile line 473
  30. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.kineticProfile_measurable line 476
  31. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.kinetic_entropy_balance line 480
  32. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.extended_dissipation_le line 499
  33. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.mass_source_zero line 547
  34. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.initialEntropyBudget line 607
  35. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.approximationEntropyBudget line 610
  36. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.uniform_entropyMoment line 614
  37. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.exists_uniform_entropy_approximation line 632
  38. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.clippedTime_fixed line 652
  39. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.density_clipped line 658
  40. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.uniform_entropyMoment_all_times line 664
  41. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.approximatingSolution line 674
  42. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.approximatingSolution_entropy line 678
  43. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.initial_integrable line 700
  44. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.characteristicSource_integrable line 706
  45. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.strong_continuity line 713
  46. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.renormalizedDensity line 737
  47. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.renormalizedSource line 741
  48. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.renormalizedIntegrand line 745
  49. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.spacetime_density_integrable line 750
  50. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.renormalizedDensity_measurable line 766
  51. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.renormalizedSource_measurable line 771
  52. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.renormalizedDensity_integrable line 776
  53. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.renormalizedSource_integrable line 782
  54. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.renormalizedIntegrand_integrable line 791
  55. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.renormalized_balance line 823
  56. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.renormalized_equation line 870
  57. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.mass_conservation line 894
  58. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.energy_conservation line 900
  59. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.momentum_coordinate_conservation line 908
  60. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.mass_tested_path line 930