OAI/MathematicalPhysics/Boltzmann/Approximation/CapHotUndamped.lean

GitHub source file

83 declarations, 0 contain sorry, 0 declared as axioms

A single measurable hot limit from the compatible local weak limits

  1. def OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.hotLimit line 29
  2. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.hotLimit_measurable line 32
  3. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.hotLimit_nonneg line 36
  4. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.hotLimit_eq_local line 39
  5. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.hotLimit_weak line 53
  6. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.hotLimit_cap line 64
  7. theorem OAI.BoltzmannNonuniqueness.Published.WeakL1Converges.congr_eventually line 94
  8. def OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.physicalHotDensity line 110
  9. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.physical_weak line 113
  10. def OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.rescaledHotSource line 143
  11. def OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.sourceError line 146
  12. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.sourceError_tendsto line 149
  13. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.eventually_source_tail_small line 159
  14. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.eventually_rescaledHotSource_upper line 167
  15. def OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.normalizedHot line 233
  16. def OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.rescaledHotForcing line 236
  17. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.normalizedHot_mild line 241
  18. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.normalizedHot_netSource line 254
  19. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.rescaledHot_eq_weighted line 265
  20. def OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.subsequence line 290
  21. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.subsequence_hotLimit line 308
  22. def OAI.BoltzmannNonuniqueness.JetCopyDatum.CapApproximation.coldTotal line 328
  23. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.CapApproximation.coldTotal_properties line 332
  24. def OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.rescaledColdDensity line 348
  25. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.rescaledColdDensity_measurable line 352
  26. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.rescaledColdDensity_bounds line 362
  27. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.rescaledColdDensity_integrable line 377
  28. def OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.cappedHot line 412
  29. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.cappedHot_measurable line 415
  30. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.cappedHot_nonneg line 420
  31. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.cappedHot_le line 424
  32. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.cappedHot_eq line 431
  33. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.cappedHot_physical_weak line 437
  34. def OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.background line 443
  35. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.background_gain_bound line 447
  36. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.background_loss_bound line 458
  37. def OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.hotKernel line 488
  38. instance OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.hotKernel_sFinite line 493
  39. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.hotKernel_apply line 497
  40. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.cappedHot_integrable line 501
  41. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.hotKernel_mass line 510
  42. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.hotKernel_mass_bound line 517
  43. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.hotKernel_finite line 526
  44. def OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.mixedKernel line 530
  45. instance OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.mixedKernel_sFinite line 536
  46. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.mixedKernel_apply line 544
  47. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.hotKernel_integral line 574
  48. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.mixedKernel_tensor line 582
  49. def OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.mixedMeasure line 591
  50. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.mixedMeasure_tensor line 597
  51. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.mixedMeasure_tensor_on_slab line 611
  52. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.mixedMeasure_finite line 626
  53. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.hotKernel_gaussian_moment line 676
  54. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.mixedKernel_gaussian_moment line 688
  55. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.mixedMeasure_gaussian_bound line 700
  56. def OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.coldKernel line 757
  57. instance OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.coldKernel_sFinite line 762
  58. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.coldKernel_apply line 766
  59. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.coldKernel_integral line 773
  60. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.coldKernel_mass line 786
  61. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.coldKernel_finite line 796
  62. def OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.rescaledColdSource line 829
  63. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.eventually_rescaledColdSource_bound line 832
  64. def OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.coldSourceDensity line 888
  65. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.coldSourceDensity_measurable line 893
  66. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.eventually_coldSourceDensity_bound line 902
  67. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.coldSourceDensity_tendsto_zero line 945
  68. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.CapApproximation.hotInitial_measurable line 990
  69. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.normalizedHot_measurable line 1001
  70. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.rescaledHotForcing_properties line 1009
  71. def OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.euclideanHot line 1049
  72. def OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.euclideanHotSource line 1052
  73. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.euclideanHotSource_eq line 1055
  74. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.hot_resolvent line 1063
  75. def OAI.BoltzmannNonuniqueness.EuclideanFlight.hotChart line 1101
  76. def OAI.BoltzmannNonuniqueness.EuclideanFlight.hotBaseVolume line 1106
  77. theorem OAI.BoltzmannNonuniqueness.EuclideanFlight.hotChart_measurePreserving line 1110
  78. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.euclideanHot_eq_chart line 1125
  79. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.physicalHotDensity_measurable line 1136
  80. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.euclidean_weak line 1143
  81. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.eventually_euclideanHot_integrable line 1174
  82. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.average_weak line 1193
  83. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.normalizedHot_undamped line 1238