OAI/MathematicalPhysics/Boltzmann/Jets/JetCoreConvergence.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

Limits of the compressed axial amplitude in thermal coordinates

  1. theorem OAI.BoltzmannNonuniqueness.JetCoreMap.axialMap_tendsto line 24
  2. theorem OAI.BoltzmannNonuniqueness.JetCoreMap.sourceFoot_tendsto line 39
  3. theorem OAI.BoltzmannNonuniqueness.JetCoreDensity.compressed_dilation line 52
  4. theorem OAI.BoltzmannNonuniqueness.JetCoreDensity.compressed_tendsto line 62
  5. theorem OAI.BoltzmannNonuniqueness.JetCoreDensity.compressed_sourceFoot_tendsto line 76
  6. theorem OAI.BoltzmannNonuniqueness.PlaneChart.join_sub line 103
  7. theorem OAI.BoltzmannNonuniqueness.PlaneChart.join_tendsto line 108
  8. theorem OAI.BoltzmannNonuniqueness.JetCoreMeasure.velocityMap_tendsto line 129
  9. theorem OAI.BoltzmannNonuniqueness.JetCoreDensity.continuous_compressed line 162
  10. theorem OAI.BoltzmannNonuniqueness.JetCoreDensity.compressed_le_scale line 172
  11. theorem OAI.BoltzmannNonuniqueness.JetCoreDensity.sourceFoot_continuous line 183
  12. theorem OAI.BoltzmannNonuniqueness.JetCoreDensity.thermal_test_tendsto line 189
  13. theorem OAI.BoltzmannNonuniqueness.JetCoreMap.sourceFoot_dilation line 263
  14. theorem OAI.BoltzmannNonuniqueness.JetCoreMap.sourceFoot_abs_le line 269
  15. theorem OAI.BoltzmannNonuniqueness.JetCoreDensity.thermal_parameter_axial_le_one line 289
  16. theorem OAI.BoltzmannNonuniqueness.JetCoreDensity.eventually_axial_cutoff line 297
  17. theorem OAI.BoltzmannNonuniqueness.JetCoreDensity.axial_cutoff_test_tendsto line 317
  18. def OAI.BoltzmannNonuniqueness.JetCoreDensity.testCoefficient line 359
  19. theorem OAI.BoltzmannNonuniqueness.JetCoreDensity.testCoefficient_measurable line 363
  20. theorem OAI.BoltzmannNonuniqueness.JetCoreDensity.testCoefficient_abs_le line 374
  21. theorem OAI.BoltzmannNonuniqueness.JetCoreDensity.testCoefficient_tendsto line 383
  22. theorem OAI.BoltzmannNonuniqueness.JetCoreDensity.thermal_coefficient_error_tendsto line 395
  23. theorem OAI.BoltzmannNonuniqueness.JetCoreDensity.masked_error_le line 451
  24. theorem OAI.BoltzmannNonuniqueness.JetCoreDensity.thermal_masked_error_tendsto line 511
  25. theorem OAI.BoltzmannNonuniqueness.JetCoreMeasure.velocityMap_dilation line 551
  26. theorem OAI.BoltzmannNonuniqueness.JetCoreDensity.weight_measurable line 561
  27. theorem OAI.BoltzmannNonuniqueness.JetCoreDensity.weight_nonneg line 574
  28. theorem OAI.BoltzmannNonuniqueness.JetCoreDensity.free_test_integral line 584
  29. theorem OAI.BoltzmannNonuniqueness.JetCoreDensity.weight_dilation line 613
  30. theorem OAI.BoltzmannNonuniqueness.JetCoreDensity.dilated_free_test_integral line 644
  31. def OAI.BoltzmannNonuniqueness.JetCoreDensity.dilatedMask line 694
  32. theorem OAI.BoltzmannNonuniqueness.JetCoreDensity.dilatedMask_measurable line 698
  33. theorem OAI.BoltzmannNonuniqueness.JetCoreDensity.dilatedMask_abs_le line 702
  34. theorem OAI.BoltzmannNonuniqueness.JetCoreDensity.dilated_free_thermal_reduction line 709
  35. def OAI.BoltzmannNonuniqueness.JetAffineSheet.center line 759
  36. def OAI.BoltzmannNonuniqueness.JetAffineSheet.affineMap line 761
  37. theorem OAI.BoltzmannNonuniqueness.JetAffineSheet.affineMap_eq line 764
  38. theorem OAI.BoltzmannNonuniqueness.JetAffineSheet.scaled_argument line 775
  39. theorem OAI.BoltzmannNonuniqueness.JetAffineSheet.gaussian_coordinate line 794
  40. theorem OAI.BoltzmannNonuniqueness.JetAffineSheet.gaussian_parameter_bound line 801
  41. theorem OAI.BoltzmannNonuniqueness.JetAffineSheet.measure_domination line 813
  42. def OAI.BoltzmannNonuniqueness.JetGeometry.scaleShell line 872
  43. theorem OAI.BoltzmannNonuniqueness.JetGeometry.measurableSet_scaleShell line 874
  44. theorem OAI.BoltzmannNonuniqueness.JetGeometry.ae_norm_ne line 878
  45. theorem OAI.BoltzmannNonuniqueness.JetGeometry.indicator_one_abs_le line 886
  46. theorem OAI.BoltzmannNonuniqueness.JetGeometry.ae_annular_indicator_tendsto line 892
  47. theorem OAI.BoltzmannNonuniqueness.JetGeometry.annular_indicator_L1_tendsto line 922
  48. def OAI.BoltzmannNonuniqueness.JetRemainderSheet.remainder line 990
  49. def OAI.BoltzmannNonuniqueness.JetRemainderSheet.amplitude line 993
  50. def OAI.BoltzmannNonuniqueness.JetRemainderSheet.uniformConstant line 996
  51. theorem OAI.BoltzmannNonuniqueness.JetRemainderSheet.remainder_eq line 1000
  52. theorem OAI.BoltzmannNonuniqueness.JetRemainderSheet.measure_domination line 1009
  53. theorem OAI.BoltzmannNonuniqueness.JetRemainderSheet.amplitude_bound line 1020
  54. theorem OAI.BoltzmannNonuniqueness.JetRemainderSheet.axial_moment line 1031
  55. theorem OAI.BoltzmannNonuniqueness.JetRemainderSheet.normalized_gain_bound line 1046
  56. def OAI.BoltzmannNonuniqueness.JetEnvelopeGain.amplitude line 1083
  57. theorem OAI.BoltzmannNonuniqueness.JetEnvelopeGain.measure_eq line 1086
  58. theorem OAI.BoltzmannNonuniqueness.JetEnvelopeGain.normalized_gain_bound line 1102
  59. theorem OAI.BoltzmannNonuniqueness.JetEnvelopeGain.amplitude_bound line 1124
  60. theorem OAI.BoltzmannNonuniqueness.JetEnvelopeGain.gain_bound line 1148
  61. theorem OAI.BoltzmannNonuniqueness.JetEnvelopeGain.thermal_width_le line 1164
  62. theorem OAI.BoltzmannNonuniqueness.JetEnvelopeGain.thermal_scale_small line 1171