OAI/MathematicalPhysics/Boltzmann/Approximation/CapColdAverages.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

The fixed-window cold truncation loses only escaped mass

  1. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.central_le_meshCold line 23
  2. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.meshCold_gap_le_escaped line 51
  3. def OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.meshColdDensity line 93
  4. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.meshCold_measurable line 98
  5. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.meshColdDensity_measurable line 111
  6. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.scaled_mesh_gap_le_escaped line 122
  7. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.meshColdDensity_sum line 168
  8. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.eventually_meshColdDensity_fixed line 186
  9. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.eventually_meshColdDensity_average line 231
  10. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.coldLabel_spacetime_weak_limit line 294
  11. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.finite_cold_spacetime_weak_limit line 349
  12. def OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.meshWindowSet line 411
  13. def OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.meshWindowVolume line 414
  14. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.meshWindowSet_measurable line 417
  15. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.eventually_mesh_gap line 421
  16. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.mesh_truncation_L1_limit line 461
  17. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.hot_spacetime_resolvent line 514
  18. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.hot_velocity_averages_resolvent line 541
  19. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.finite_cold_spacetime_background_limit line 578
  20. theorem OAI.BoltzmannNonuniqueness.JetPeriodicDatum.spatialMap_join line 622
  21. def OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.meshColdChartAverage line 636
  22. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.eventually_meshColdChartAverage line 640
  23. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.mesh_cold_spacetime_background_limit line 651
  24. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.meshColdDensity_bounds line 693
  25. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.meshColdChart_fiber_integrable line 712
  26. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.meshColdChartAverage_measurable line 727
  27. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.meshColdChartAverage_global_bound line 739
  28. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.meshColdChartAverage_integrable line 758
  29. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.eventually_cold_mesh_average_error line 789
  30. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.cold_mesh_average_L1_limit line 839
  31. theorem OAI.BoltzmannNonuniqueness.SheetMeasures.norm_join_le_add line 885
  32. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.cold_away_axis_weak_limit line 895