OAI/MathematicalPhysics/Boltzmann/Compactness/PeriodicWeakCompactness.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

Localized renormalized characteristics in Euclidean coordinates

  1. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.projectedPhase line 36
  2. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.projected_characteristic line 38
  3. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.euclideanRenormalizedDensity line 48
  4. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.euclideanRenormalizedSource line 52
  5. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.renormalized_localized_path line 56
  6. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.euclidean_renormalized_localized line 83
  7. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.euclideanRenormalizedDensity_measurable line 126
  8. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.euclideanRenormalizedSource_measurable line 133
  9. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.approximatingSolution_renormalizedFields_cell_uniformIntegrable line 140
  10. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.approximatingSolution_renormalizedLocalizedSource_uniformIntegrable line 172
  11. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.renormalized_resolvent line 198
  12. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.renormalized_average_resolvent line 216
  13. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.approximatingSolution_renormalized_average_compactness line 242
  14. structure OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalWeakLimit line 295
  15. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.exists_globalWeakLimit line 304
  16. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalWeakLimit.weak_on_window line 320
  17. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.approximatingSolution_rational_averages_uniform line 340
  18. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.approximatingSolution_density_average_compactness line 389
  19. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.exists_globalWeakLimit_refining line 482
  20. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.approximatingSolution_countable_density_averages line 514
  21. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalWeakLimit.kineticProfile line 634
  22. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalWeakLimit.kineticProfile_measurable line 638
  23. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalWeakLimit.kinetic_weak_on_window line 642
  24. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalWeakLimit.lifted_weak_on_window line 652
  25. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalWeakLimit.average_weak_on_window line 663
  26. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalWeakLimit.average_weak line 698
  27. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalWeakLimit.average_strong_identification line 719
  28. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.approximatingSolution_normalizedPair_compactness line 766
  29. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalWeakLimit.subsequence line 786
  30. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalWeakLimit.exists_normalizedPair_limit line 795
  31. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.exists_globalWeakLimit_with_averages line 832
  32. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.approximatingSolution_patch_velocity_tail line 894
  33. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.exists_globalWeakLimit_patch_averages line 949
  34. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.weak_pair_on_window line 1014
  35. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.normalizedPair_lift line 1036
  36. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.normalizedPair_lifted_weak line 1040
  37. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.approximatingSolution_cell_entropy_integrable line 1074
  38. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.approximatingSolution_cell_entropy_le line 1087
  39. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.approximatingSolution_cell_mass_uniformIntegrable line 1108
  40. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.relativeEntropy_of_weak_approximation line 1135
  41. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalWeakLimit.entropy_on_window line 1154
  42. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalWeakLimit.entropyMoment_on_window line 1162
  43. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalWeakLimit.finiteEntropy_ae line 1169
  44. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.relativeEntropy_of_weak_approximation_sharp line 1192
  45. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalWeakLimit.entropy_ae line 1221
  46. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalWeakLimit.finiteEntropy_ae_volume line 1243