OAI/MathematicalPhysics/Boltzmann/Jets/GeometricTwoCoreUniform.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.BoltzmannNonuniqueness.GeometricMesh.exists_retained_scale_list line 21

   Source documentation

   The cardinality bound is independent of the dilation and cutoff index.

   theorem exists_retained_scale_list {s₀ η r μ R : ℝ} (hs₀ : 0 < s₀) (hη : 0 < η)
       (hr : 0 < r) (hμ : 0 < μ) (N : ℕ) :
       ∃ S : Finset ℝ, S.card ≤ (Finset.Icc (index (μ/Real.exp η) η) (index R η)).card ∧
         ∀ j < N, μ ≤ JetGeometry.jetScale s₀ η j/r →
           JetGeometry.jetScale s₀ η j/r ≤ R → JetGeometry.jetScale s₀ η j/r ∈ S := by
   …

   Mentions: OAI.BoltzmannNonuniqueness.GeometricMesh.index, OAI.BoltzmannNonuniqueness.JetGeometry.jetScale

2. theorem OAI.BoltzmannNonuniqueness.GeometricMesh.retained_thermal_width_le line 35
3. theorem OAI.BoltzmannNonuniqueness.GeometricMesh.retained_thermal_width_tendsto line 44
4. abbrev OAI.BoltzmannNonuniqueness.JetCoreSheet.MeshLabel line 70
5. def OAI.BoltzmannNonuniqueness.JetCoreSheet.meshScale line 72
6. theorem OAI.BoltzmannNonuniqueness.JetCoreSheet.geometric_thermal_five_tendsto line 75
7. theorem OAI.BoltzmannNonuniqueness.JetCoreSheet.geometric_two_core_axial_tendsto line 130
8. def OAI.BoltzmannNonuniqueness.JetCoreSheet.geometricTwoCoreMass line 194
9. theorem OAI.BoltzmannNonuniqueness.JetCoreSheet.geometric_two_core_uniform line 219
10. theorem OAI.BoltzmannNonuniqueness.JetCoreSheet.geometric_two_core_time_tendsto line 247