OAI/MathematicalPhysics/Boltzmann/Compactness/UniformGain.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BoltzmannNonuniqueness.UniformGain.exponentialTilt line 26
2. theorem OAI.BoltzmannNonuniqueness.UniformGain.measurable_exponentialTilt line 28
3. theorem OAI.BoltzmannNonuniqueness.UniformGain.measurable_weightRatio line 32
4. theorem OAI.BoltzmannNonuniqueness.UniformGain.ratio_bound line 35
5. theorem OAI.BoltzmannNonuniqueness.UniformGain.normalized_restriction_le line 54

   Source documentation

   The weight transfer can be applied on any measurable portion of the chart.

   theorem normalized_restriction_le (c : Measure Velocity) (q : ℝ) (v : Velocity)
       {S T : Set Coordinates} (hS : MeasurableSet S) (hT : MeasurableSet T)
       (hST : S ⊆ T) {B : ℝ} (hB : 0 ≤ B)
       (hb : ∀ y ∈ S,
         Real.exp (-‖companionVelocity y.1 (chart v y.1 y.2.1 y.2.2) v‖ ^ 2) ≤ B) :
       normalizedMeasure c q v S ≤ ENNReal.ofReal (tiltConstant * B) *
         ChartKernel.measure (c.withDensity exponentialTilt) (weightRatio q v) v T := by
   …

   Mentions: OAI.BoltzmannNonuniqueness.Velocity, OAI.BoltzmannNonuniqueness.companionVelocity, OAI.BoltzmannNonuniqueness.ChartKernel.measure, OAI.BoltzmannNonuniqueness.UniformGain.exponentialTilt

6. theorem OAI.BoltzmannNonuniqueness.UniformGain.measurableSet_ballRegion line 81
7. theorem OAI.BoltzmannNonuniqueness.UniformGain.weight_ball_measure_bound line 84
8. def OAI.BoltzmannNonuniqueness.UniformGain.ballBound line 92
9. theorem OAI.BoltzmannNonuniqueness.UniformGain.tilted_ball_bound line 95
10. theorem OAI.BoltzmannNonuniqueness.UniformGain.tilted_tail_ball_bound line 107
11. theorem OAI.BoltzmannNonuniqueness.UniformGain.normalized_ball_bound line 126
12. def OAI.BoltzmannNonuniqueness.UniformGain.radius line 139
13. def OAI.BoltzmannNonuniqueness.UniformGain.shell line 142
14. def OAI.BoltzmannNonuniqueness.UniformGain.incomingTail line 145
15. def OAI.BoltzmannNonuniqueness.UniformGain.companionTail line 147
16. theorem OAI.BoltzmannNonuniqueness.UniformGain.measurable_radius line 150
17. theorem OAI.BoltzmannNonuniqueness.UniformGain.measurableSet_shell line 153
18. theorem OAI.BoltzmannNonuniqueness.UniformGain.measurableSet_incomingTail line 157
19. theorem OAI.BoltzmannNonuniqueness.UniformGain.measurableSet_companionTail line 160
20. theorem OAI.BoltzmannNonuniqueness.UniformGain.shell_subset_ball line 166
21. theorem OAI.BoltzmannNonuniqueness.UniformGain.shell_subset_union line 171
22. theorem OAI.BoltzmannNonuniqueness.UniformGain.normalized_cold_shell_bound line 180
23. theorem OAI.BoltzmannNonuniqueness.UniformGain.normalized_hot_shell_bound line 201
24. theorem OAI.BoltzmannNonuniqueness.UniformGain.normalized_shell_bound_raw line 217
25. def OAI.BoltzmannNonuniqueness.UniformGain.shellConstant line 234
26. theorem OAI.BoltzmannNonuniqueness.UniformGain.geometricTotalConstant_nonneg line 237
27. theorem OAI.BoltzmannNonuniqueness.UniformGain.shellConstant_nonneg line 242
28. theorem OAI.BoltzmannNonuniqueness.UniformGain.shell_coefficient_bound line 248
29. theorem OAI.BoltzmannNonuniqueness.UniformGain.normalized_shell_bound line 282

    Source documentation

    The full normalized kernel has a uniform Gaussian bound on every shell.

    theorem normalized_shell_bound {q d R L : ℝ} (hq₁ : 1 < q) (hq₂ : q < 2)
        (hd : 0 ≤ d) (hdmax : d ≤ 1 / 8) (hR : 1 ≤ R)
        {v : Velocity} (hv : transverse v ≠ 0) {ρ : Measure ℝ} [IsProbabilityMeasure ρ]
        (hρ : AxialMoment ρ L) :
        normalizedMeasure (sheetLaw d ρ) q v (shell v R) ≤
          ENNReal.ofReal (shellConstant q L * R ^ 2 * Real.exp (-(3 / 32) * R ^ 2)) :=
    …

    Mentions: OAI.BoltzmannNonuniqueness.Velocity, OAI.BoltzmannNonuniqueness.UniformGain.shell, OAI.BoltzmannNonuniqueness.UniformGain.shellConstant