OAI/MathematicalPhysics/Boltzmann/Branching/TwoCoreLimit.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.BoltzmannNonuniqueness.GainPullback.integral_three_regions_le line 25

   Source documentation

   Exceptional axial intervals and transverse tails use the total kernel bound; the remaining region uses the small second-kernel mass.

   theorem integral_three_regions_le (μ : Measure X) {E T : Set X}
       (hE : MeasurableSet E) (hT : MeasurableSet T) {f : X → ℝ≥0∞}
       {B ε : ℝ≥0∞} (hB : ∀ x, f x ≤ B)
       (hgood : ∀ x, x ∉ E → x ∉ T → f x ≤ ε) :
       (∫⁻ x, f x ∂μ) ≤ B*μ E+B*μ T+ε*μ univ := by
   …

2. theorem OAI.BoltzmannNonuniqueness.GainPullback.integral_three_regions_tendsto line 55

   Source documentation

   This criterion only uses explicit mass bounds for the two discarded regions and a pointwise bound on the remaining second-kernel mass.

   theorem integral_three_regions_tendsto {μ : ℕ → Measure X} {f : ℕ → X → ℝ≥0∞}
       {B C : ℝ≥0∞} (hB : B ≠ ∞) (hC : C ≠ ∞)
       (hbound : ∀ n x, f n x ≤ B) (hmass : ∀ n, μ n univ ≤ C)
       (hregions : ∀ ε : ℝ≥0∞, 0 < ε → ∀ᶠ n in atTop, ∃ E T : Set X,
         MeasurableSet E ∧ MeasurableSet T ∧ μ n E ≤ ε ∧ μ n T ≤ ε ∧
         ∀ x, x ∉ E → x ∉ T → f n x ≤ ε) :
       Tendsto (fun n => ∫⁻ x, f n x ∂μ n) atTop (𝓝 0) := by
   …

3. theorem OAI.BoltzmannNonuniqueness.GainPullback.two_kernel_weighted_le line 94
4. theorem OAI.BoltzmannNonuniqueness.GainPullback.two_kernel_weighted_tendsto line 104
5. theorem OAI.BoltzmannNonuniqueness.GainPullback.two_time_integral_le line 117

   Source documentation

   Uniform smallness survives both time integrations. No measurability of the parameter dependence is needed for this upper bound.

   theorem two_time_integral_le {f : ℝ → ℝ → ℝ≥0∞} {a T : ℝ} {ε : ℝ≥0∞}
       (hf : ∀ t₁ ∈ Ioc a T, ∀ t₂ ∈ Ioc a t₁, f t₁ t₂ ≤ ε) :
       (∫⁻ t₁ in Ioc a T, ∫⁻ t₂ in Ioc a t₁, f t₁ t₂) ≤
         ε*(volume (Ioc a T))^2 := by
   …

6. theorem OAI.BoltzmannNonuniqueness.GainPullback.two_time_uniform_tendsto line 137
7. def OAI.BoltzmannNonuniqueness.JetCoreSheet.ballisticSecondCoreMass line 171
8. theorem OAI.BoltzmannNonuniqueness.JetCoreSheet.two_core_small_regions line 179

   Source documentation

   The small-scale threshold precedes the cardinality and large-scale radius. This is the order of choices in the two-axial-gains lemma of §8.

   theorem two_core_small_regions {K α γ q a ε : ℝ} (hK : 0 ≤ K)
       (hα : 0 < α) (hγ : 0 < γ) (hq₁ : 1 < q) (hq₂ : q < 2)
       (ha : 0 < a) (hε : 0 < ε) :
       ∃ μ₀ : ℝ, 0 < μ₀ ∧ ∀ J : ℕ, ∃ d₀ r₀ : ℝ, 0 < d₀ ∧ 0 < r₀ ∧
         ∀ {s₁ d₁ t₁ t₂ : ℝ}, 0 < s₁ → 0 < d₁ → d₁ ≤ 1/16 →
         a ≤ t₂ → t₂ ≤ t₁ →
         ∀ (η : ℝ) (sign₁ : Bool) (x : JetPrototype.Space) (v : Velocity)
           (S : Finset ℝ) (s₂ d₂ : Velocity → ℝ)
           (sign₂ : Velocity → Bool) (y₂ : Velocity → Transverse),
         ‖transverse v‖ ≤ r₀ → S.card ≤ J →
         (∀ w, 0 < s₂ w) → (∀ w, 0 < d₂ w) → (∀ w, d₂ w ≤ 1/16) →
         (∀ w, d₂ w ≤ d₀) → (∀ w, μ₀ ≤ s₂ w → s₂ w ∈ S) →
   …

   Mentions: OAI.BoltzmannNonuniqueness.JetPrototype.Space, OAI.BoltzmannNonuniqueness.Velocity

9. theorem OAI.BoltzmannNonuniqueness.PositiveIteration.step_add_kernel line 271
10. theorem OAI.BoltzmannNonuniqueness.PositiveIteration.iterate_two_add_self line 278
11. def OAI.BoltzmannNonuniqueness.PositiveIteration.pairMass line 308
12. theorem OAI.BoltzmannNonuniqueness.PositiveIteration.integrate_second_step line 312
13. theorem OAI.BoltzmannNonuniqueness.PositiveIteration.iterate_two_eq_pairMass line 321
14. theorem OAI.BoltzmannNonuniqueness.JetCoreSheet.two_core_axial_tendsto line 352

    Source documentation

    This is the velocity-integral part of the two-axial-gains lemma. The finite list hypothesis is a scale-discretization condition, with no integral or compactness conclusion assumed. Both collision times and positions may vary.

    theorem two_core_axial_tendsto {K α γ q a : ℝ} (hK : 0 ≤ K)
        (hα : 0 < α) (hγ : 0 < γ) (hq₁ : 1 < q) (hq₂ : q < 2) (ha : 0 < a)
        (η s₁ d₁ t₁ t₂ D : ℕ → ℝ) (sign₁ : ℕ → Bool)
        (x : ℕ → JetPrototype.Space) (v : ℕ → Velocity)
        (s₂ d₂ : ℕ → Velocity → ℝ) (sign₂ : ℕ → Velocity → Bool)
        (y₂ : ℕ → Velocity → Transverse)
        (hs₁ : ∀ n, 0 < s₁ n) (hd₁ : ∀ n, 0 < d₁ n) (hd₁max : ∀ n, d₁ n ≤ 1/16)
        (ht₂ : ∀ n, a ≤ t₂ n) (htt : ∀ n, t₂ n ≤ t₁ n)
        (hs₂ : ∀ n w, 0 < s₂ n w) (hd₂ : ∀ n w, 0 < d₂ n w)
        (hd₂max : ∀ n w, d₂ n w ≤ 1/16) (hd₂D : ∀ n w, d₂ n w ≤ D n)
        (hD : Tendsto D atTop (𝓝 0))
        (hv : Tendsto (fun n => ‖transverse (v n)‖) atTop (𝓝 0))
    …

    Mentions: OAI.BoltzmannNonuniqueness.JetPrototype.Space, OAI.BoltzmannNonuniqueness.Velocity