The cutoff-multiplied zoom fields: smoothness, axis, divergence, and the drift limit #
For a shrinking zoom scale lam n → 0⁺ and a moving axial offset zc n uniformly bounded by
ζ < 1, this file builds, for every n, the globally smooth fields
Vseq n := cutoffBump h zc hzc hζ (lam n) (hlam0 n) n * (zoomV (lam n) h (zc n) u ·, -1))
Wseq n := cutoffBump h zc hzc hζ (lam n) (hlam0 n) n * (zoomW (lam n) h (zc n) u ·, -1))
and proves each of the hypotheses of CIV.step_finite_contradiction other than the selection
bound hlower, which belongs to the (separately tracked) dichotomy argument that selects
Rsel and c₀:
hVsmooth,hWsmooth: globalContDiff ℝ (⊤ : ℕ∞), for everyn— the repair this file is for; the raw zoom slices are smooth only on the preimage ofunitCylinderat scalelam n, centrezc n(CIV.FiniteZoomCutoffField), and the cutoff makes the product globally smooth by vanishing identically outside a compact subset of that preimage.haxis:Vseq n (0, 0) = 0for everyn, fromCIV.zoomV_axisand axisymmetry.hdivn: the finite-ndivergence identityCIV.zoom_divergence_identity, transported toVseq/Wseqbecause the cutoff equals1near any fixed off-axis point oncenis large.hdWn:∂_R W_n → 0, from the potential-vorticity identityCIV.zoomOmega_eqapplied pointwise (not merely in the limit):∂_R W_n = lam^{4h} ∂_Z V_n − R Ω_n, and the first summand→ 0becauselam^{4h} → 0while∂_Z V_nstays bounded (CIV.abs_dz_zoomV_le), so∂_R W_n → 0onceΩ_n → 0is supplied (the endpoint vanishing of the comparison argument,CIV/Zoom/ZoomLimitEndpoint.lean, taken here as a hypothesis at the same moving centrezc n).
The zoom centre zc : ℕ → ℝ is one axial offset per stage, uniformly bounded by a single
ζ < 1 (hzc, hζ) rather than fixed for every n: the finite-axis selection this adapter is
eventually fed (CIV.exists_seq_three_terms_dichotomy) returns a moving height sequence, not a
single real number.
The cutoff-multiplied fields #
The cutoff-multiplied radial field at stage n.
Equations
- CIV.cutoffZoomV h zc hzc hζ u lam hlam0 n q = ↑(CIV.cutoffBump h zc hzc hζ (lam n) ⋯ n) q * CIV.zoomV (lam n) h (zc n) u (q, -1)
Instances For
The cutoff-multiplied vertical field at stage n.
Equations
- CIV.cutoffZoomW h zc hzc hζ u lam hlam0 n q = ↑(CIV.cutoffBump h zc hzc hζ (lam n) ⋯ n) q * CIV.zoomW (lam n) h (zc n) u (q, -1)
Instances For
The cutoff equals 1 throughout any bounded square, eventually #
For every compact bound r, once n is large enough that the cutoff's inner radius
exceeds r, the cutoff equals 1 throughout the sup-ball of radius r, so Vseq n (resp.
Wseq n) equals the raw zoom slice there and the raw slice's own dr/dz bounds transfer
directly.
The cutoff's own smoothness, restricted to the sup-ball where it equals 1, is enough to
transport a HasFDerivAt fact of the raw slice to the cutoff-multiplied field: on that open
ball the two functions agree pointwise, so their derivatives agree too.
Global smoothness #
The raw radial zoom slice at scale lam and centre zc is ContDiffOn ℝ (⊤ : ℕ∞) on the
preimage of unitCylinder under the zoom map, because it is lam times the zeroth component of
u composed with the globally smooth zoomPoint map, and u itself is smooth wherever the
zoom point lands.
hVsmooth: for every n, Vseq n is globally ContDiff ℝ (⊤ : ℕ∞).
hWsmooth: for every n, Wseq n is globally ContDiff ℝ (⊤ : ℕ∞).
The axis value #
haxis: Vseq n (0, 0) = 0 for every n, since the cutoff is 1 at the origin (its
inner radius is always positive) and zoomV vanishes on the axis of an axisymmetric field.
Eventually the cutoff-multiplied field's derivative reads off the raw slice #
Once n is large enough that the cutoff equals 1 on a neighbourhood of p, the raw
radial zoom slice has a Fréchet derivative at p equal to that of the cutoff-multiplied
field: the two functions agree on that whole open neighbourhood, so their derivatives agree,
by HasFDerivAt.congr_of_eventuallyEq applied to the globally smooth Vseq n's own derivative
(CIV.contDiff_cutoffZoomV, unpacked through contDiff_infty_iff_fderiv).
The vertical counterpart of eventually_hasFDerivAt_zoomV_slice.
The cutoff-multiplied field's radial derivative reads off dr of the raw slice, once n
is large enough.
The cutoff-multiplied field's axial derivative reads off dz of the raw slice, once n
is large enough.
The cutoff-multiplied vertical field's radial derivative reads off dr of the raw slice,
once n is large enough.
The cutoff-multiplied field's radial derivative also reads off dr of the raw slice for
Wseq, and the value at p reads off the raw slice, once n is large enough: the three
facts a single application of zoom_divergence_identity needs.
The drift limit ∂_R W_n → 0, from Ω_n → 0 #
Once n is large enough that the zoom point at p lands in unitCylinder, it stays
there: this is the same threshold eventually_cutoffBump_rIn_gt supplies for the cutoff's
inner radius, chained through cutoffBump_safe.
The sandwich estimate for a sequence that is only eventually bounded: if a n → 0 and
|D n| ≤ M for all large n, then a n * D n → 0. The eventual form is needed here
because the pointwise bound on dz (zoomV …) is only available once the zoom point at the
fixed test point p has entered unitCylinder.
hdWn: the radial derivative of the cutoff-multiplied vertical field tends to 0, once
Ω_n → 0 at p, along the same moving centre zc n, is supplied. The pointwise
potential-vorticity identity CIV.zoomOmega_eq gives, at every large n,
dr (zoomW …) = lam ^ (4h) dz (zoomV …) − R Ω_n: the first summand tends to 0 because
lam ^ (4h) → 0 while dz (zoomV …) stays uniformly bounded (CIV.abs_dz_zoomV_le), and the
second because Ω_n → 0 by hypothesis.