OAI/MathematicalPhysics/Boltzmann/Branching/DilatedTwoCoreLimit.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.BoltzmannNonuniqueness.ChartKernel.inputKernel_smul_base line 27
2. def OAI.BoltzmannNonuniqueness.JetCoreSheet.rescaledCoreMeasure line 41
3. theorem OAI.BoltzmannNonuniqueness.JetCoreSheet.amplitude_dilation line 46
4. theorem OAI.BoltzmannNonuniqueness.JetCoreSheet.rescaledCoreMeasure_axis line 54
5. theorem OAI.BoltzmannNonuniqueness.JetCoreSheet.dilatedFreeKernel_eq_rescaled line 60
6. theorem OAI.BoltzmannNonuniqueness.JetCoreSheet.rescaled_region_le line 84
7. theorem OAI.BoltzmannNonuniqueness.JetCoreSheet.rescaled_mass_bound line 116
8. theorem OAI.BoltzmannNonuniqueness.JetCoreSheet.rescaled_axial_bands line 132
9. theorem OAI.BoltzmannNonuniqueness.JetCoreSheet.rescaled_axis_input line 149
10. theorem OAI.BoltzmannNonuniqueness.JetCoreSheet.rescaled_speed_gap line 168
11. theorem OAI.BoltzmannNonuniqueness.JetCoreSheet.rescaled_bands_small_of_card line 206

    Source documentation

    The radius is uniform in the interval centers, core scale, and thermal width.

    theorem rescaled_bands_small_of_card {K α γ q a ε : ℝ} (hK : 0 ≤ K)
        (hα : 0 < α) (hγ : 0 < γ) (hq₁ : 1 < q) (hq₂ : q < 2)
        (ha : 0 < a) (hε : 0 < ε) (N : ℕ) :
        ∃ δ : ℝ, 0 < δ ∧ ∀ {r s d t : ℝ}, 0 < r → 0 < s → 0 < d → d ≤ 1/16 → a ≤ t →
          ∀ (η : ℝ) (sign : Bool) (x : JetPrototype.Space) (v : Velocity) (S : Finset ℝ),
          S.card ≤ N →
          rescaledCoreMeasure r η K α γ s d q sign t x v
            (axial ⁻¹' bands S δ) ≤ ENNReal.ofReal ε := by
    …

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

12. theorem OAI.BoltzmannNonuniqueness.JetCoreSheet.rescaled_away_small_of_transverse line 242
13. theorem OAI.BoltzmannNonuniqueness.JetCoreSheet.rescaled_small_input line 285
14. theorem OAI.BoltzmannNonuniqueness.JetCoreSheet.rescaled_axial_decay line 335
15. theorem OAI.BoltzmannNonuniqueness.JetCoreSheet.rescaled_large_output line 380
16. theorem OAI.BoltzmannNonuniqueness.JetRemainderSheet.uniformConstant_nonneg line 423
17. theorem OAI.BoltzmannNonuniqueness.JetRemainderSheet.thermal_amplitude_bound line 429
18. theorem OAI.BoltzmannNonuniqueness.JetRemainderSheet.dilated_gain_bound line 441
19. theorem OAI.BoltzmannNonuniqueness.JetRemainderSheet.remainder_gain_majorant_tendsto_zero line 458
20. theorem OAI.BoltzmannNonuniqueness.JetCoreSheet.rescaled_velocity_tail line 486
21. theorem OAI.BoltzmannNonuniqueness.JetCoreSheet.rescaled_second_core_small_off_bands line 549
22. def OAI.BoltzmannNonuniqueness.JetCoreSheet.rescaledBallisticSecondCoreMass line 604
23. theorem OAI.BoltzmannNonuniqueness.JetCoreSheet.rescaled_two_core_small_regions line 612

    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 rescaled_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₀ ∧
          ∀ {R s₁ d₁ t₁ t₂ : ℝ}, 0 < R → 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

24. theorem OAI.BoltzmannNonuniqueness.JetCoreSheet.rescaled_two_core_small_integral line 698
25. theorem OAI.BoltzmannNonuniqueness.JetCoreSheet.rescaled_two_core_axial_tendsto line 777

    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 rescaled_two_core_axial_tendsto {K α γ q a : ℝ} (hK : 0 ≤ K)
        (hα : 0 < α) (hγ : 0 < γ) (hq₁ : 1 < q) (hq₂ : q < 2) (ha : 0 < a)
        (R η s₁ d₁ t₁ t₂ D : ℕ → ℝ) (sign₁ : ℕ → Bool)
        (x : ℕ → JetPrototype.Space) (v : ℕ → Velocity)
        (s₂ d₂ : ℕ → Velocity → ℝ) (sign₂ : ℕ → Velocity → Bool)
        (y₂ : ℕ → Velocity → Transverse)
        (hR : ∀ n, 0 < R n) (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