OAI/MathematicalPhysics/Boltzmann/Jets/JetSupersolutions.lean

GitHub source file

85 declarations, 0 contain sorry, 0 declared as axioms

The full logarithmic barrier derivative along free flights

  1. def OAI.BoltzmannNonuniqueness.JetLogDerivative.Y line 27
  2. def OAI.BoltzmannNonuniqueness.JetLogDerivative.Z line 30
  3. def OAI.BoltzmannNonuniqueness.JetLogDerivative.rawExponent line 33
  4. def OAI.BoltzmannNonuniqueness.JetLogDerivative.logSlope line 37
  5. theorem OAI.BoltzmannNonuniqueness.JetLogDerivative.rawExponent_eq line 43
  6. theorem OAI.BoltzmannNonuniqueness.JetLogDerivative.rawExponent_derivative line 52
  7. theorem OAI.BoltzmannNonuniqueness.JetLogDerivative.distance_gradient_bound line 70
  8. theorem OAI.BoltzmannNonuniqueness.JetLogDerivative.logSlope_lower line 92
  9. theorem OAI.BoltzmannNonuniqueness.JetLogDerivative.ae_logarithmic_derivative line 102
  10. def OAI.BoltzmannNonuniqueness.JetBarrierDerivative.along line 137
  11. def OAI.BoltzmannNonuniqueness.JetBarrierDerivative.amplitude line 140
  12. theorem OAI.BoltzmannNonuniqueness.JetBarrierDerivative.along_eq line 143
  13. theorem OAI.BoltzmannNonuniqueness.JetBarrierDerivative.squaredError_eq line 148
  14. theorem OAI.BoltzmannNonuniqueness.JetBarrierDerivative.ae_barrier_derivative line 154

    Source documentation

    Manuscript inequality (4.7), almost everywhere on each free characteristic.

    theorem ae_barrier_derivative {K α γ s d : ℝ} (hK : 0 ≤ K) (hα : 0 ≤ α) (hγ : 0 ≤ γ)
    (hs : 0 < s) (hd : 0 < d) (η : ℝ) (a : Bool) (p : JetPrototype.Phase) :
    ∀ᵐ t, 0 < t → t ≤ 2 →
      HasDerivAt (along η K α γ s d a p) (deriv (along η K α γ s d a p) t) t ∧
        (1 + (7 / 8 : ℝ) * ‖JetCoreFlight.error α γ s t a p‖ ^ 2 / d ^ 2) *
          along η K α γ s d a p t ≤ deriv (along η K α γ s d a p) t := by
…

    Mentions: OAI.BoltzmannNonuniqueness.JetPrototype.Phase, OAI.BoltzmannNonuniqueness.JetBarrierDerivative.along, OAI.BoltzmannNonuniqueness.JetCoreFlight.error

  15. def OAI.BoltzmannNonuniqueness.JetSupersolution.epsilon line 197
  16. def OAI.BoltzmannNonuniqueness.JetSupersolution.U line 199
  17. theorem OAI.BoltzmannNonuniqueness.JetSupersolution.epsilon_nonneg line 202
  18. theorem OAI.BoltzmannNonuniqueness.JetSupersolution.nonneg line 206
  19. theorem OAI.BoltzmannNonuniqueness.JetSupersolution.le_twice_barrier line 211
  20. theorem OAI.BoltzmannNonuniqueness.JetSupersolution.measurable_velocity line 220
  21. theorem OAI.BoltzmannNonuniqueness.JetSupersolution.gain_bound line 225
  22. def OAI.BoltzmannNonuniqueness.JetSupersolution.along line 248
  23. theorem OAI.BoltzmannNonuniqueness.JetSupersolution.along_eq line 251
  24. theorem OAI.BoltzmannNonuniqueness.JetSupersolution.ae_supersolution line 258

    Source documentation

    The supersolution inequality used in Proposition prop:cold-control. The only smallness condition here is the explicit thermal-width condition.

    theorem ae_supersolution {K s d α γ : ℝ} (hK : 0 ≤ K) (hs : 0 < s) (hd : 0 < d)
    (hα : 0 ≤ α) (hγ : 0 ≤ γ) (hε : epsilon K s d ≤ 1)
    (η : ℝ) (a : Bool) (p : JetPrototype.Phase) (z : Position) :
    ∀ᵐ t, 0 < t → t ≤ 1 →
      HasDerivAt (along η K α γ s d a p) (deriv (along η K α γ s d a p) t) t ∧
        gain (fun q => U η K α γ s d t a ((flight t p).1, q.2)) z p.2 ≤
          deriv (along η K α γ s d a p) t := by
…

    Mentions: OAI.BoltzmannNonuniqueness.JetSupersolution.epsilon, OAI.BoltzmannNonuniqueness.JetPrototype.Phase, OAI.BoltzmannNonuniqueness.Position, OAI.BoltzmannNonuniqueness.JetSupersolution.along, OAI.BoltzmannNonuniqueness.gain, OAI.BoltzmannNonuniqueness.JetSupersolution.U

  25. theorem OAI.BoltzmannNonuniqueness.JetCoreMeasure.jacobian_measurable line 305
  26. theorem OAI.BoltzmannNonuniqueness.JetCoreMeasure.axial_measurePreserving line 312
  27. theorem OAI.BoltzmannNonuniqueness.JetCoreMeasure.transverse_measurePreserving line 329
  28. def OAI.BoltzmannNonuniqueness.JetCoreMeasure.parameterMeasure line 338
  29. def OAI.BoltzmannNonuniqueness.JetCoreMeasure.velocityMap line 342
  30. theorem OAI.BoltzmannNonuniqueness.JetCoreMeasure.velocity_measurePreserving line 345
  31. theorem OAI.BoltzmannNonuniqueness.JetCoreMeasure.parameterMeasure_eq line 353
  32. theorem OAI.BoltzmannNonuniqueness.JetCoreMeasure.map_withDensity line 365
  33. theorem OAI.BoltzmannNonuniqueness.CollisionCutoff.frequency_le_majorant_ae line 397
  34. theorem OAI.BoltzmannNonuniqueness.CollisionCutoff.frequency_le_majorant line 416
  35. theorem OAI.BoltzmannNonuniqueness.JetSupersolution.cutoff_frequency_bound line 439
  36. theorem OAI.BoltzmannNonuniqueness.JetSupersolution.core_cutoff_frequency_bound line 479
  37. theorem OAI.BoltzmannNonuniqueness.JetSupersolution.core_frequency_along line 497
  38. theorem OAI.BoltzmannNonuniqueness.JetCoreDensity.thermal_argument line 532
  39. def OAI.BoltzmannNonuniqueness.JetCoreDensity.compressed line 561
  40. def OAI.BoltzmannNonuniqueness.JetCoreDensity.weight line 564
  41. theorem OAI.BoltzmannNonuniqueness.JetCoreDensity.density_identity line 569
  42. theorem OAI.BoltzmannNonuniqueness.JetCoreDensity.compressed_nonneg line 616
  43. theorem OAI.BoltzmannNonuniqueness.JetCoreDensity.compressed_bound line 623
  44. theorem OAI.BoltzmannNonuniqueness.JetCoreDensity.weight_bound line 630
  45. theorem OAI.BoltzmannNonuniqueness.JetCoreDensity.measure_identity line 648
  46. def OAI.BoltzmannNonuniqueness.JetEnvelopeBound.amplitude line 699
  47. theorem OAI.BoltzmannNonuniqueness.JetEnvelopeBound.amplitude_nonneg line 702
  48. theorem OAI.BoltzmannNonuniqueness.JetEnvelopeBound.barrier_le line 708
  49. def OAI.BoltzmannNonuniqueness.JetEnvelopeBound.gainAmplitude line 733
  50. theorem OAI.BoltzmannNonuniqueness.JetEnvelopeBound.gainAmplitude_nonneg line 736
  51. theorem OAI.BoltzmannNonuniqueness.JetEnvelopeBound.gain_bound line 743
  52. theorem OAI.BoltzmannNonuniqueness.JetEnvelopeBound.integrable_gain line 770
  53. theorem OAI.BoltzmannNonuniqueness.JetEnvelopeBound.cutoff_gain_bound line 780
  54. theorem OAI.BoltzmannNonuniqueness.JetEnvelopeBound.U_le_H line 790
  55. theorem OAI.BoltzmannNonuniqueness.JetBarrierRegularity.profile_lipschitz line 840
  56. theorem OAI.BoltzmannNonuniqueness.JetBarrierRegularity.square_ac line 848
  57. theorem OAI.BoltzmannNonuniqueness.JetBarrierRegularity.exp_ac line 854
  58. theorem OAI.BoltzmannNonuniqueness.JetBarrierRegularity.flightFoot_ac line 863
  59. theorem OAI.BoltzmannNonuniqueness.JetBarrierRegularity.flightVelocity_ac line 871
  60. theorem OAI.BoltzmannNonuniqueness.JetBarrierRegularity.rawExponent_ac line 880
  61. theorem OAI.BoltzmannNonuniqueness.JetBarrierRegularity.barrier_ac line 909
  62. def OAI.BoltzmannNonuniqueness.JetTimeRegularity.positiveFoot line 936
  63. theorem OAI.BoltzmannNonuniqueness.JetTimeRegularity.positiveFoot_distance line 939
  64. theorem OAI.BoltzmannNonuniqueness.JetTimeRegularity.continuous_positiveFoot line 950
  65. def OAI.BoltzmannNonuniqueness.JetTimeRegularity.positiveU line 962
  66. theorem OAI.BoltzmannNonuniqueness.JetTimeRegularity.positiveU_eq line 966
  67. theorem OAI.BoltzmannNonuniqueness.JetTimeRegularity.measurable_positiveU line 970
  68. theorem OAI.BoltzmannNonuniqueness.JetBarrierTrace.barrier_monotone line 1017
  69. theorem OAI.BoltzmannNonuniqueness.JetBarrierTrace.barrier_right_limit line 1035
  70. theorem OAI.BoltzmannNonuniqueness.JetBarrierTrace.supersolution_right_limit line 1054

    Source documentation

    A finite initial trace exists and dominates the initial color. An explicit formula for the trace on spatial boundaries is unnecessary.

    theorem supersolution_right_limit {K α γ s d : ℝ} (hK : 0 ≤ K) (hα : 0 ≤ α) (hγ : 0 ≤ γ)
    (hs : 0 < s) (hd : 0 < d) (η : ℝ) (label : Bool) (p : JetPrototype.Phase) :
    ∃ l : ℝ, density η K α γ s d label p ≤ l ∧
      Tendsto (JetSupersolution.along η K α γ s d label p) (𝓝[>] 0) (𝓝 l) := by
…

    Mentions: OAI.BoltzmannNonuniqueness.JetPrototype.Phase, OAI.BoltzmannNonuniqueness.JetSupersolution.along

  71. theorem OAI.BoltzmannNonuniqueness.JetBarrierTrace.supersolution_ac line 1068
  72. theorem OAI.BoltzmannNonuniqueness.JetAxialLaw.axialMap_abs_le line 1098
  73. def OAI.BoltzmannNonuniqueness.JetAxialLaw.law line 1107
  74. theorem OAI.BoltzmannNonuniqueness.JetAxialLaw.probability line 1110
  75. theorem OAI.BoltzmannNonuniqueness.JetAxialLaw.moment line 1114
  76. def OAI.BoltzmannNonuniqueness.JetGaussianProduct.density line 1147
  77. def OAI.BoltzmannNonuniqueness.JetGaussianProduct.coefficient line 1150
  78. theorem OAI.BoltzmannNonuniqueness.JetGaussianProduct.density_eq line 1152
  79. theorem OAI.BoltzmannNonuniqueness.JetGaussianProduct.density_nonneg line 1161
  80. theorem OAI.BoltzmannNonuniqueness.JetGaussianProduct.kernel_bound line 1165
  81. theorem OAI.BoltzmannNonuniqueness.JetGaussianProduct.gaussian_scaling line 1187
  82. theorem OAI.BoltzmannNonuniqueness.JetGaussianProduct.gaussianLaw_map_smul line 1196
  83. def OAI.BoltzmannNonuniqueness.JetGaussianProduct.parameterLaw line 1223
  84. theorem OAI.BoltzmannNonuniqueness.JetGaussianProduct.parameterLaw_density line 1226
  85. theorem OAI.BoltzmannNonuniqueness.JetGaussianProduct.parameterLaw_map line 1236