OAI/MathematicalPhysics/Boltzmann/Collision/GaussianLocalExistence.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.timeWeight line 19
2. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.finiteTimeMeasure line 20
3. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.timeWeight_measurable line 22
4. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.timeWeight_pos line 24
5. instance OAI.BoltzmannNonuniqueness.PeriodicApproximation.finiteTimeMeasure_finite line 26
6. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.windowInverseWeight line 33
7. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.windowInverseWeight_measurable line 35
8. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.windowInverseWeight_nonneg line 38
9. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.windowInverseWeight_bound line 41
10. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.finiteTimeMeasure_reweight line 51
11. def OAI.BoltzmannNonuniqueness.GaussianLocal.state line 86
12. def OAI.BoltzmannNonuniqueness.GaussianLocal.forcing line 89
13. theorem OAI.BoltzmannNonuniqueness.GaussianLocal.measurable_state line 93
14. theorem OAI.BoltzmannNonuniqueness.GaussianLocal.measurable_forcing line 96
15. theorem OAI.BoltzmannNonuniqueness.GaussianLocal.measurable_flight line 100
16. theorem OAI.BoltzmannNonuniqueness.GaussianLocal.exists_normalized line 104
17. theorem OAI.BoltzmannNonuniqueness.GaussianCutoff.gain_family_summable line 159
18. theorem OAI.BoltzmannNonuniqueness.GaussianCutoff.tsum_coldSource line 173
19. theorem OAI.BoltzmannNonuniqueness.GaussianCutoff.hot_source_identity line 186
20. theorem OAI.BoltzmannNonuniqueness.GaussianLocal.normalized_unique line 214
21. def OAI.BoltzmannNonuniqueness.GaussianLocal.physical line 270
22. theorem OAI.BoltzmannNonuniqueness.GaussianLocal.physical_source line 273
23. theorem OAI.BoltzmannNonuniqueness.GaussianLocal.time_eq line 286
24. theorem OAI.BoltzmannNonuniqueness.GaussianLocal.physical_mild line 290
25. theorem OAI.BoltzmannNonuniqueness.GaussianLocal.exists_normalized_time line 314
26. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.cutoffExtendedDissipation_regularization_le_liminf line 359
27. theorem OAI.BoltzmannNonuniqueness.GaussianLocal.exists_positive_mild line 440

    Source documentation

    A bounded Gaussian datum has a positive mild solution for a positive time. The constant damping is added and subtracted inside the exact collision source.

    theorem exists_positive_mild {β b A : ℝ} (hβ : 0 < β) (hb : 0 ≤ b) (hA : 0 < A)
        {g₀ : JetPrototype.Phase → ℝ} (hg₀m : Measurable g₀)
        (hg₀ : ∀ p, 0 ≤ g₀ p ∧ g₀ p ≤ A * JetGaussianMoments.kernel β p.2) :
        ∃ T L : ℝ, 0 < T ∧ 0 ≤ L ∧
          ∃ g : ℝ × JetPrototype.Phase → ℝ, Measurable g ∧
            (∀ z, 0 ≤ g z ∧ g z ≤ (2 * A) * JetGaussianMoments.kernel β z.2.2) ∧
            (∀ t ∈ Icc 0 T, ∀ p, g (t, p) =
              Real.exp (-L * t) * g₀ (JetBarrier.flight (-t) p) +
              ∫ r in 0..t, Real.exp (-L * (t - r)) *
                (CollisionCutoff.gain b
                  (fun v => g (r, ((JetBarrier.flight (r-t) p).1, v))) p.2 +
                (L - CollisionCutoff.frequency b
    …

    Mentions: OAI.BoltzmannNonuniqueness.JetPrototype.Phase, OAI.BoltzmannNonuniqueness.JetGaussianMoments.kernel, OAI.BoltzmannNonuniqueness.JetBarrier.flight, OAI.BoltzmannNonuniqueness.CollisionCutoff.gain, OAI.BoltzmannNonuniqueness.CollisionCutoff.frequency