OAI/MathematicalPhysics/Boltzmann/Approximation/CapNonlinearHotLimit.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Global L¹ convergence for every chosen compact interior hot average

  1. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.global_strong_averages line 40
  2. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.strong_average_products line 99
  3. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotPairExtraction.factorized_moments line 172
  4. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotPairExtraction.pairLimit_eq_product line 235
  5. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.normalizedHot_cap_at line 329
  6. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.normalizedHot_cap_backward line 341
  7. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotPairExtraction.nonlinear_weak line 375
  8. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.exists_hot_nonlinear_limit line 394
  9. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotPairExtraction.weighted_nonlinear_subsequence line 433
  10. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotPairExtraction.pairLimit_eq_capped_product line 512
  11. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotPairExtraction.capped_pair_weak line 541
  12. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotPairExtraction.strong_all_hot_averages line 579
  13. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.euclideanHot_nonneg line 660
  14. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotPairExtraction.collision_subsequence line 667
  15. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotPairExtraction.vanishing_quadratic_subsequence line 719
  16. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.eventually_physicalHot_cylinder_integrable line 768
  17. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.eventually_hotSource_cylinder_integrable line 786
  18. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotPairExtraction.vanishing_collision_error line 826
  19. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.zero_euclidean_L1 line 885
  20. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.zero_boundedHotRatio_L1 line 897
  21. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.zero_physical_L1 line 941
  22. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.zero_physical_inMeasure line 953
  23. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.zero_ratio_L1 line 983
  24. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.zero_ratio_inMeasure line 995