OAI/MathematicalPhysics/Boltzmann/Collision/AxialBandMeasure.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BoltzmannNonuniqueness.AxialFlow.collapsedCenters line 17
2. def OAI.BoltzmannNonuniqueness.AxialFlow.profileCenters line 20
3. def OAI.BoltzmannNonuniqueness.AxialFlow.bands line 23
4. theorem OAI.BoltzmannNonuniqueness.AxialFlow.outside_bands line 26
5. theorem OAI.BoltzmannNonuniqueness.AxialFlow.collapsedCenters_card_le line 31
6. theorem OAI.BoltzmannNonuniqueness.AxialFlow.profileCenters_card_le line 36
7. theorem OAI.BoltzmannNonuniqueness.AxialFlow.outside_profileBands_second_gap line 49

   Source documentation

   A single finite list excludes every large retained scale at the second time.

   theorem outside_profileBands_second_gap {α γ b t₁ t₂ z w s d ω : ℝ}
       (hα : 0 ≤ α) (hγ : 0 ≤ γ) (hs : 0 < s) (ht₂ : 0 ≤ t₂) (htt : t₂ ≤ t₁)
       (S : Finset ℝ) (hsS : s ∈ S) (hw : w ∉ bands (profileCenters α γ t₁ z S) b)
       (herr : |d*ω| ≤ b/2) (σ : ℝ) (hσ : σ = 1 ∨ σ = -1) :
       b/2 ≤ |w-JetCoreMap.axialMap σ α γ s d t₂ (z-(t₁-t₂)*w) ω| := by
   …

   Mentions: OAI.BoltzmannNonuniqueness.AxialFlow.bands, OAI.BoltzmannNonuniqueness.AxialFlow.profileCenters, OAI.BoltzmannNonuniqueness.JetCoreMap.axialMap

8. theorem OAI.BoltzmannNonuniqueness.AxialFlow.outside_collapsedBands_second_gap line 61

   Source documentation

   Five collapsed speeds exclude every sufficiently small positive scale.

   theorem outside_collapsedBands_second_gap {α γ a δ : ℝ}
       (hα : 0 < α) (hγ : 0 < γ) (ha : 0 < a) (hδ : 0 < δ) :
       ∃ μ₀ : ℝ, 0 < μ₀ ∧ ∀ (σ s d t₁ t₂ z w ω : ℝ),
         (σ = 1 ∨ σ = -1) → 0 < s → s < μ₀ → a ≤ t₂ → t₂ ≤ t₁ → |d*ω| < δ/4 →
         w ∉ bands (collapsedCenters α t₁ z) δ →
         δ/2 ≤ |w-JetCoreMap.axialMap σ α γ s d t₂ (z-(t₁-t₂)*w) ω| := by
   …

   Mentions: OAI.BoltzmannNonuniqueness.AxialFlow.bands, OAI.BoltzmannNonuniqueness.AxialFlow.collapsedCenters, OAI.BoltzmannNonuniqueness.JetCoreMap.axialMap

9. theorem OAI.BoltzmannNonuniqueness.AxialFlow.bands_measurableSet line 95
10. theorem OAI.BoltzmannNonuniqueness.AxialFlow.bands_measure_le line 99
11. theorem OAI.BoltzmannNonuniqueness.JetCoreSheet.core_axial_bands line 118

    Source documentation

    The first gain charges a finite exceptional-speed list by its cardinality times one uniform small-interval bound. The centers may depend on the endpoint.

    theorem core_axial_bands {α q ε : ℝ} (hq₁ : 1 < q) (hq₂ : q < 2) (hε : 0 < ε) :
        ∃ δ : ℝ, 0 < δ ∧ ∀ {K γ s d t : ℝ}, 0 ≤ K → 0 < α → 0 < γ →
          0 < s → 0 < d → d ≤ 1/16 → 0 ≤ t → ∀ (η : ℝ) (a : Bool)
          (x : JetPrototype.Space) (v : Velocity), transverse v ≠ 0 → ∀ S : Finset ℝ,
          normalizedCoreKernel η K α γ s d q a ((t,x),v) (axial ⁻¹' bands S δ) ≤
            S.card*(ENNReal.ofReal (amplitude K α γ s t)*ENNReal.ofReal ε) := by
    …

    Mentions: OAI.BoltzmannNonuniqueness.JetPrototype.Space, OAI.BoltzmannNonuniqueness.Velocity, OAI.BoltzmannNonuniqueness.JetCoreSheet.normalizedCoreKernel, OAI.BoltzmannNonuniqueness.JetCoreSheet.amplitude