TranslatedTwoCoreLimit.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Two-core convergence in the physical periodic-copy coordinates

theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.copyFreeKernel_eq_rescaled line 15
theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.axial_flight_translation line 23

theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.copy_two_core_axial_tendsto line 30

Source documentation

The selected second label can vary with the intermediate velocity. This statement covers the retained paths based at one periodic origin.

theorem copy_two_core_axial_tendsto {K α γ q a s₀ η d₀ M : ℝ}
    (hK : 0 ≤ K) (hα : 0 < α) (hγ : 0 < γ) (hq₁ : 1 < q) (hq₂ : q < 2)
    (ha : 0 < a) (hs₀ : 0 < s₀) (hsmax : s₀ ≤ 1/8) (hη : 0 < η)
    (hd₀ : 0 < d₀) (hdmax : d₀ ≤ 1)
    (r t₁ t₂ : ℕ → ℝ) (N : ℕ → ℕ) (i₁ : ℕ → Label) (i₂ : ℕ → Velocity → Label)
    (x : ℕ → Velocity) (v : ℕ → Velocity)
    (hr : ∀ n, 0 < r n) (hrlim : Tendsto r atTop (𝓝 0))
    (ht₂ : ∀ n, a ≤ t₂ n) (htt : ∀ n, t₂ n ≤ t₁ n)
    (hi₂ : ∀ n w, (i₂ n w).annulus < N n)
    (hscale : ∀ n w, JetGeometry.jetScale s₀ η (i₂ n w).annulus/r n ≤ M)
    (hcopy : ∀ n w, (i₂ n w).lattice = (i₁ n).lattice)
    (hv : Tendsto (fun n => ‖transverse (v n)‖) atTop (𝓝 0)) :
…

Mentions: OAI.BoltzmannNonuniqueness.Velocity, OAI.BoltzmannNonuniqueness.JetGeometry.jetScale