OAI/MathematicalPhysics/Boltzmann/Approximation/CapColdBounds.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

Half-Gaussian moments of the actual cold part

  1. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.CapApproximation.cold_envelope line 29
  2. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.CapApproximation.coldTotal_moment_bound line 52
  3. theorem OAI.BoltzmannNonuniqueness.VelocityMoment.moment_const_mul line 111
  4. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.rescaledColdDensity_moment line 126
  5. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.eventually_rescaledColdDensity_moment line 153
  6. theorem OAI.BoltzmannNonuniqueness.JetLattice.measurableSet_spatialEnlargement line 195
  7. def OAI.BoltzmannNonuniqueness.JetCopyDatum.CapApproximation.escapedTotal line 211
  8. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.CapApproximation.escapedTotal_measurable line 216
  9. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.CapApproximation.escapedTotal_nonneg line 245
  10. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.CapApproximation.escapedTotal_bound line 258
  11. def OAI.BoltzmannNonuniqueness.JetCopyDatum.CapApproximation.centralTotal line 304
  12. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.CapApproximation.centralTotal_measurable line 310
  13. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.CapApproximation.coldTotal_eq_central_add_escaped line 332
  14. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.CapApproximation.centralTotal_single line 373
  15. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.CapApproximation.cold_free_majorant_at_main line 408
  16. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.CapApproximation.coldTotal_eq_escaped_of_no_main line 431
  17. def OAI.BoltzmannNonuniqueness.JetCopyDatum.centralLabels line 462
  18. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.mem_centralLabels line 466
  19. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.CapApproximation.centralTotal_finite line 480
  20. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.CapApproximation.centralTotal_finite_pairs line 499
  21. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.centralTotal_mesh_window line 533
  22. def OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.rescaledEscapedDensity line 598
  23. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.rescaledEscapedDensity_measurable line 603
  24. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.rescaledEscapedDensity_nonneg line 612
  25. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.eventually_rescaledEscapedDensity_bound line 620
  26. def OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.coldSlabSet line 659
  27. def OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.coldSlabVolume line 662
  28. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.coldSlabVolume_eq line 665
  29. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.rescaledEscapedDensity_tendsto_zero line 671
  30. def OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.rescaledCentralDensity line 719
  31. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.rescaledCentralDensity_measurable line 724
  32. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.rescaledCold_sub_central line 733
  33. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.cold_central_difference_tendsto_zero line 751
  34. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.escaped_bound_global line 785
  35. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.normalized_escaped_bound_global line 824
  36. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.CapApproximation.escapedTotal_bound_global line 851
  37. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.euclideanHot_measurable line 899
  38. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.euclideanHotSource_measurable line 905
  39. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.eventually_euclideanHot_bound line 923
  40. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.eventually_euclideanHotSource_bound line 959
  41. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.coldLabelDensity_le_total line 999
  42. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.eventually_coldLabelAverage_bound line 1015
  43. def OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.coldAverage line 1069
  44. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.coldAverage_measurable line 1073
  45. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.coldAverage_global_bound line 1081
  46. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.coldAverage_integrable line 1097
  47. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.eventually_coldAverage_bound line 1106
  48. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.coldLabelDensity_joint_measurable line 1151
  49. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.coldLabelAverage_joint_measurable line 1163
  50. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.coldLabelAverage_global_bound line 1172
  51. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.coldLabelAverage_joint_integrable line 1189
  52. def OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.meshLabels line 1218
  53. def OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.meshCold line 1221
  54. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.meshCold_sum line 1226
  55. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.meshCold_le_total line 1249