OAI/MathematicalPhysics/Boltzmann/Approximation/CapLabelFreeLimit.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

Actual weak hot limits on bounded spacetime windows

  1. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.exists_hot_weak_limit line 31
  2. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.hotWindow_time_mem line 74
  3. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.hotDensity_cap_bound line 79
  4. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.hot_velocity_integrable line 98
  5. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.hot_time_majorant_integrable line 106
  6. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.hot_weak_limit_cap line 115
  7. structure OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction line 152
  8. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.exists_hot_limit_extraction line 172
  9. def OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.coldLabel line 229
  10. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.coldLabel_scale_limit line 233
  11. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.coldLabel_retained line 240
  12. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.coldLabel_scale_tendsto_zero line 248
  13. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.coldLabel_width_tendsto_zero line 255
  14. def OAI.BoltzmannNonuniqueness.JetCopyDatum.CapApproximation.cold line 281
  15. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.CapApproximation.local_free_error line 285
  16. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.coldLabel_at_endpoint line 339
  17. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.coldLabel_below_endpoint line 350
  18. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.coldLabel_retained_iff line 362
  19. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.cap_cold_dilation_free_error line 397
  20. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.cap_variable_cold_dilation_free_error line 491
  21. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.coldLabel_mask_average_limit line 587
  22. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.coldLabel_mask_average_integrable line 617
  23. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.CapApproximation.cold_properties line 648
  24. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.CapApproximation.hotNetSource_measurable line 675
  25. def OAI.BoltzmannNonuniqueness.JetCopyDatum.CapApproximation.hotInitial line 703
  26. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.CapApproximation.hot_mild line 709
  27. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.CapApproximation.hot_localized line 731
  28. def OAI.BoltzmannNonuniqueness.JetCopyDatum.CapApproximation.coldSource line 773
  29. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.CapApproximation.coldSource_measurable line 777
  30. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.CapApproximation.cold_source_bound line 787
  31. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.coldLabel_thermal_limit line 852
  32. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.coldLabel_thermal_L1_limit line 907
  33. def OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.coldLabelFreeAverage line 984
  34. def OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.coldLabelStripeAverage line 990
  35. def OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.coldLabelStripedProfile line 998
  36. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.coldLabel_free_striped_L1_limit line 1005
  37. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.cap_variable_cold_dilation_limit line 1084
  38. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.cap_variable_cold_L1_dilation_limit line 1137
  39. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.coldLabel_free_limit line 1194