Eventual circulation-bound companions for the uniform swirl vanishing #
theorem tendstoUniformlyOn_zoomSRec_of_tendsto_circulation_bound_of_eventual is the
eventual analogue of tendstoUniformlyOn_zoomSRec_of_tendsto_circulation_bound; its circulation
hypothesis hΓ is only required for sufficiently large n, matching the true in-domain
circulation bound eq:aniso:zoom:circulation which holds eventually in n once lamSeq n is
small enough to keep the zoom point inside the domain.
The two pointwise corollaries consume that uniform result: the first specialises it to a
singleton set and extracts a Tendsto … atTop (nhds 0) at a single point, which is the
one-point conclusion that the finite-axis and receding-axis contradictions of the proof of
prop:aniso:small need.
theorem
CIV.tendstoUniformlyOn_zoomSRec_of_tendsto_circulation_bound_of_eventual
{h zc CΓ : ℝ}
(u : ℕ → CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3)
(lamSeq rcSeq : ℕ → ℝ)
(hlam : ∀ (n : ℕ), 0 < lamSeq n)
(hlam0 : Filter.Tendsto lamSeq Filter.atTop (nhds 0))
{K : Set (ℝ × ℝ)}
(hK : IsCompact K)
{M : ℕ → ℝ}
(hMpos : ∀ (n : ℕ), 0 < M n)
(hMtop : Filter.Tendsto M Filter.atTop Filter.atTop)
(hKM : ∀ (n : ℕ), ∀ y ∈ K, M n ≤ rcSeq n / lamSeq n + y.1)
{Z : ℝ}
(hCΓ : 0 ≤ CΓ)
(hΓ :
∀ᶠ (n : ℕ) in Filter.atTop, ∀ y ∈ K, |circulation (u n) (zoomPointRec (lamSeq n) h (rcSeq n) zc ((y.1, y.2), Z))| ≤ CΓ)
(hh : 0 ≤ h)
:
theorem
CIV.tendsto_zoomSRec_atPoint_of_tendstoUniformlyOn
{h : ℝ}
(u : ℕ → CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3)
(lamSeq rcSeq : ℕ → ℝ)
(zc : ℝ)
{K : Set (ℝ × ℝ)}
{Z : ℝ}
(hunif :
TendstoUniformlyOn (fun (n : ℕ) (y : ℝ × ℝ) => zoomSRec (lamSeq n) h (rcSeq n) zc (u n) ((y.1, y.2), Z))
(fun (x : ℝ × ℝ) => 0) Filter.atTop K)
{y : ℝ × ℝ}
(hy : y ∈ K)
:
theorem
CIV.tendsto_zoomSRec_atPoint_of_tendsto_circulation_bound_of_eventual
{h zc CΓ : ℝ}
(u : ℕ → CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3)
(lamSeq rcSeq : ℕ → ℝ)
(hlam : ∀ (n : ℕ), 0 < lamSeq n)
(hlam0 : Filter.Tendsto lamSeq Filter.atTop (nhds 0))
{M : ℕ → ℝ}
(hMpos : ∀ (n : ℕ), 0 < M n)
(hMtop : Filter.Tendsto M Filter.atTop Filter.atTop)
{y : ℝ × ℝ}
(hyM : ∀ (n : ℕ), M n ≤ rcSeq n / lamSeq n + y.1)
{Z : ℝ}
(hCΓ : 0 ≤ CΓ)
(hΓ : ∀ᶠ (n : ℕ) in Filter.atTop, |circulation (u n) (zoomPointRec (lamSeq n) h (rcSeq n) zc (y, Z))| ≤ CΓ)
(hh : 0 ≤ h)
: