OAI/MathematicalPhysics/Boltzmann/Approximation/SubcapMildLimits.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.BelowCap.cap_family_gainLoss_uniformIntegrable line 28
2. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.BelowCap.cap_family_cutoff_uniformIntegrable line 57
3. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.BelowCap.cap_family_density_uniformIntegrable line 95
4. structure OAI.BoltzmannNonuniqueness.JetCopyDatum.BelowCap.CompactFamily line 139
5. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.BelowCap.CompactFamily.source_ui line 159
6. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.BelowCap.CompactFamily.density_ui_cell line 186
7. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.BelowCap.CompactFamily.source_ui_cell line 195
8. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.BelowCap.Approximation.spacetime_mild line 222
9. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.BelowCap.Approximation.characteristic_slice line 256
10. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.BelowCap.CompactFamily.raw_pairs_ui_cell line 293
11. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.BelowCap.CompactFamily.localized_source_ui line 326
12. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.BelowCap.CompactFamily.averaging_subsequence line 352
13. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.BelowCap.Approximation.averages_resolvent line 393
14. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.BelowCap.CompactFamily.physical_averages_subsequence line 410
15. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.BelowCap.capped_family_unifTight line 444
16. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.BelowCap.cap_family_unifTight line 484
17. structure OAI.BoltzmannNonuniqueness.JetCopyDatum.BelowCap.TightFamily line 533
18. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.BelowCap.uniformIntegrable_comp line 563
19. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.BelowCap.TightFamily.exists_weak_limits line 569
20. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.BelowCap.CompactFamily.countable_physical_averages line 614
21. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.BelowCap.TightFamily.exists_weak_and_average_limits line 646
22. def OAI.BoltzmannNonuniqueness.JetCopyDatum.BelowCap.averageWeight line 691
23. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.BelowCap.TightFamily.exists_factorized_pair_moments line 694
24. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.BelowCap.TightFamily.exists_nonlinear_weak_limit line 762

    Source documentation

    The velocity-averaging step identifies the genuine nonlinear pair product.

    theorem TightFamily.exists_nonlinear_weak_limit
        (hcarleman : Published.GPV2009CarlemanInput) (hGLPS : Published.GLPS1988Proposition3)
        (hDP : Published.DunfordPettis1940Theorem321)
        {s₀ η K α γ d₀ q : ℝ} (F : TightFamily s₀ η K α γ d₀ q)
        (hq₁ : 1 < q) (hq₂ : q < 2) :
        ∃ (φ : ℕ → ℕ) (g : (ℝ × Position) × Velocity → ℝ), StrictMono φ ∧
          Published.WeakL1Converges ((AnnularEnvelope.timePositionVolume F.time).prod volume)
            (fun n => torusPhysical q (F.approximation (φ n)).solution.value) g ∧
          Published.WeakL1Converges ((AnnularEnvelope.timePositionVolume F.time).prod volume)
            (fun n => CollisionCompactness.pairProduct
              (torusPhysical q (F.approximation (φ n)).solution.value))
            (CollisionCompactness.pairProduct g) ∧
    …

    Mentions: OAI.BoltzmannNonuniqueness.Published.GPV2009CarlemanInput, OAI.BoltzmannNonuniqueness.Published.GLPS1988Proposition3, OAI.BoltzmannNonuniqueness.Published.DunfordPettis1940Theorem321, OAI.BoltzmannNonuniqueness.JetCopyDatum.BelowCap.TightFamily, OAI.BoltzmannNonuniqueness.Position, OAI.BoltzmannNonuniqueness.Velocity, OAI.BoltzmannNonuniqueness.Published.WeakL1Converges, OAI.BoltzmannNonuniqueness.AnnularEnvelope.timePositionVolume, OAI.BoltzmannNonuniqueness.JetCopyDatum.torusPhysical, OAI.BoltzmannNonuniqueness.CollisionCompactness.pairProduct

25. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.BelowCap.TightFamily.exists_weighted_nonlinear_weak_limit line 863
26. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.BelowCap.TightFamily.exists_positive_nonlinear_limit line 926
27. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.BelowCap.TightFamily.exists_cutoff_equation_limit_with_pair line 965
28. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.BelowCap.TightFamily.exists_cutoff_equation_limit line 1007
29. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.BelowCap.CompactFamily.initial_weak_limit line 1040
30. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.BelowCap.TightFamily.exists_mild_limit_with_convergence line 1070
31. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.BelowCap.TightFamily.exists_mild_limit line 1130
32. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.BelowCap.TightFamily.weak_each_time line 1162
33. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.BelowCap.TightFamily.exists_mild_limit_with_traces_and_convergence line 1192
34. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.BelowCap.TightFamily.exists_mild_limit_with_time_traces line 1214