Receding-branch compactness at a moving zoom centre #
The receding zoom of the proof of prop:aniso:small is taken about the selected points
x_n = (r_n, z_n), which move with n (eq:aniso:zoom:receding:variables). This module restates
the time-pairing estimate for the rescaled vorticity quotient at a moving centre (rc n, zc n)
with r_n / λ_n → ∞, using the circulation bound only on the window B(R_*) × (t_*, 0) of
eq:aniso:zoom:circulation, and concludes the locally uniform convergence of the rescaled
quotients on ℝ² × (−∞, −1] along a subsequence.
theorem
CIV.forceTerm_pairing_bound_fixed_moving
{h lam rc zc M : ℝ}
(hh0 : 0 < h)
(hlam_pos : 0 < lam)
(hlam_le : lam ≤ 1)
{f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(hMnn : 0 ≤ M)
(hMmax :
∀ z ∈ unitCylinder,
∀ (i : Fin 3) (α : Fin 3 → ℕ),
α 0 + α 1 + α 2 ≤ 2 → |multiPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => f w i) α z| ≤ M)
{K : Set (ℝ × ℝ)}
(hK : IsCompact K)
(τ : ℝ)
(hmem : ∀ y ∈ K, zoomPointRec lam h rc zc (y, τ) ∈ unitCylinder)
(ψ : ℝ × ℝ → ℝ)
:
ContDiff ℝ (↑⊤) ψ →
HasCompactSupport ψ →
∀ (hψU : tsupport ψ ⊆ interior K) (B : ℝ),
0 ≤ B →
∀ (hψB : ∀ (y : ℝ × ℝ), |ψ y| ≤ B ∧ ‖fderiv ℝ ψ y‖ ≤ B ∧ ‖fderiv ℝ (fderiv ℝ ψ) y‖ ≤ B),
|∫ (y : ℝ × ℝ), lam ^ 4 * lam ^ (2 * h) * curlComp f 1 (zoomPointRec lam h rc zc (y, τ)) * ψ y| ≤ 2 * M * (MeasureTheory.volume K).toReal * B
theorem
CIV.eventually_mem_zoomPointRec_moving
{h ρ Rstar tstar : ℝ}
(hh : 0 < h ∧ h < 1 / 2)
(hρ0 : 0 ≤ ρ)
(hρ : ρ < Rstar)
(htstar : tstar < 0)
{rc zc : ℕ → ℝ}
(hcz : ∀ (n : ℕ), rc n ^ 2 + zc n ^ 2 ≤ ρ ^ 2)
{lam : ℕ → ℝ}
(hlam_lim : Filter.Tendsto lam Filter.atTop (nhdsWithin 0 (Set.Ioi 0)))
(K : Set ((ℝ × ℝ) × ℝ))
(hK : IsCompact K)
(hKt : ∀ p ∈ K, p.2 < 0)
:
∀ᶠ (n : ℕ) in Filter.atTop, ∀ p ∈ K,
(zoomPointRec (lam n) h (rc n) (zc n) p).1 ∈ CKN.Foundation.Parabolic.vec3Ball 0 Rstar ∧ (zoomPointRec (lam n) h (rc n) (zc n) p).2 ∈ Set.Ioo tstar 0
theorem
CIV.hpair_zoomTheta_eventual_moving
{C h CΓ ρ Rstar tstar : ℝ}
(hh : 0 < h ∧ h < 1 / 2)
(hρ0 : 0 ≤ ρ)
(hρR : ρ < Rstar)
(hR1 : Rstar ≤ 1)
(htstar : tstar < 0)
{rc zc : ℕ → ℝ}
(hcz : ∀ (n : ℕ), rc n ^ 2 + zc n ^ 2 ≤ ρ ^ 2)
(hCnn : 0 ≤ C)
(hCΓnn : 0 ≤ CΓ)
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(haniso : AnisotropicBounds C h u)
(hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder)
{pr : CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
{f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(hsol : IsClassicalSolutionOn u pr f unitCylinder)
(haxi : IsAxisymmetricOn u unitCylinder)
(hΓ : ∀ x ∈ CKN.Foundation.Parabolic.vec3Ball 0 Rstar, ∀ t ∈ Set.Ioo tstar 0, |circulation u (x, t)| ≤ CΓ)
(hforce : ForceC2Bounded f)
(lam : ℕ → ℝ)
(hlam_pos : ∀ (n : ℕ), 0 < lam n)
(hlam_lim : Filter.Tendsto lam Filter.atTop (nhdsWithin 0 (Set.Ioi 0)))
(hA : Filter.Tendsto (fun (n : ℕ) => rc n / lam n) Filter.atTop Filter.atTop)
(K : Set (ℝ × ℝ))
:
IsCompact K →
∀ (J : Set ℝ),
IsCompact J →
(∀ τ ∈ J, τ ≤ -1) →
∃ (Cₒ : ℝ),
0 ≤ Cₒ ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (ψ : ℝ × ℝ → ℝ),
ContDiff ℝ (↑⊤) ψ →
HasCompactSupport ψ →
tsupport ψ ⊆ interior K →
∀ (B : ℝ),
0 ≤ B →
(∀ (y : ℝ × ℝ), |ψ y| ≤ B ∧ ‖fderiv ℝ ψ y‖ ≤ B ∧ ‖fderiv ℝ (fderiv ℝ ψ) y‖ ≤ B) →
∀ τ ∈ J,
∀ τ' ∈ J,
|∫ (y : ℝ × ℝ), (zoomTheta (lam n) h (rc n) (zc n) u (y, τ) - zoomTheta (lam n) h (rc n) (zc n) u (y, τ')) * ψ y| ≤ Cₒ * B * |τ - τ'|
hpair for zoomTheta at the paper's MOVING centre x_n = (rc n, zc n), with the
circulation bound only on the window B(R_*) × (t_*, 0) of eq:aniso:zoom:circulation.
theorem
CIV.eventually_zoomPointRec_mem_unitCylinder_moving
{h ρ : ℝ}
(hh : 0 < h ∧ h < 1 / 2)
(hρ0 : 0 ≤ ρ)
(hρ1 : ρ < 1)
{rc zc : ℕ → ℝ}
(hcz : ∀ (n : ℕ), rc n ^ 2 + zc n ^ 2 ≤ ρ ^ 2)
(lam : ℕ → ℝ)
(hlam_lim : Filter.Tendsto lam Filter.atTop (nhdsWithin 0 (Set.Ioi 0)))
(K : Set (ℝ × ℝ))
(hK : IsCompact K)
(J : Set ℝ)
(hJ : IsCompact J)
(hJs : ∀ τ ∈ J, τ ≤ -1)
:
∀ᶠ (n : ℕ) in Filter.atTop, ∀ y ∈ K, ∀ τ ∈ J, zoomPointRec (lam n) h (rc n) (zc n) (y, τ) ∈ unitCylinder
theorem
CIV.exists_subseq_tendstoUniformlyOn_zoomTheta_moving
{C h CΓ ρ Rstar tstar : ℝ}
(hh : 0 < h ∧ h < 1 / 2)
(hρ0 : 0 ≤ ρ)
(hρR : ρ < Rstar)
(hR1 : Rstar ≤ 1)
(htstar : tstar < 0)
{rc zc : ℕ → ℝ}
(hcz : ∀ (n : ℕ), rc n ^ 2 + zc n ^ 2 ≤ ρ ^ 2)
(hCnn : 0 ≤ C)
(hCΓnn : 0 ≤ CΓ)
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(haniso : AnisotropicBounds C h u)
(hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder)
{pr : CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
{f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(hsol : IsClassicalSolutionOn u pr f unitCylinder)
(haxi : IsAxisymmetricOn u unitCylinder)
(hΓ : ∀ x ∈ CKN.Foundation.Parabolic.vec3Ball 0 Rstar, ∀ t ∈ Set.Ioo tstar 0, |circulation u (x, t)| ≤ CΓ)
(hforce : ForceC2Bounded f)
(lam : ℕ → ℝ)
(hlam_pos : ∀ (n : ℕ), 0 < lam n)
(hlam_lim : Filter.Tendsto lam Filter.atTop (nhdsWithin 0 (Set.Ioi 0)))
(hA : Filter.Tendsto (fun (n : ℕ) => rc n / lam n) Filter.atTop Filter.atTop)
:
The compactness statement at the paper's moving centre, circulation on the window only.