R2-R: the residual of the rescaled receding vorticity-quotient equation tends to zero

The receding-branch analogue of CIV.tendsto_finResidual (CIV/Zoom/FiniteResidual.lean) at (m, d) = (2, 1): against a test function φ on Vec 2 × (-∞, -1), the pairing of the rescaled azimuthal vorticity Θ_n with the adjoint operator of eq:aniso:zoom:receding:limit tends to zero along the receding zoom sequence.

The weak form comes from CIV.zoomTheta_pde (CIV/Zoom/RecedingEquation.lean), rearranged so that the drift-divergence pairing CIV.integral_recedingResidual_eq (a receding-axis, axis-singularity-free analogue of CIV.integral_liftedResidual_eq) applies directly: every term of eq:aniso:zoom:receding:equation outside the limit operator is collected into the swirl flux S_n²/(A_n+R) (whose ∂_Z reproduces the swirl-source term) and a source G_n bundling the ∂_R Θ_n/(A_n+R) term, the two curvature terms, and the force term. Each of the three pieces of the weak-form remainder — δ_n² ∫ Θ_n ∂_ZZ ψ, -∫ (S_n²/(A_n+R)) ∂_Z ψ, and ∫ G_n ψ — is bounded by a constant times a factor tending to 0 uniformly on tsupport ψ as n → ∞, since A_n = r_n/λ_n → ∞ and δ_n = λ_n^{2h} → 0.

The weak form of a drift-diffusion equation on Vec 2 × ℝ off a closed set

theorem CIV.sum_fin_two_ite_lt_one (a : Fin 2 → ℝ) : (∑ i : Fin 2, if ↑i < 1 then a i else 0) = a 0

The sum of the single term of a Fin 2-indexed masked sum with cutoff 1, the receding analogue of sum_fin_five_ite_lt_four.

theorem CIV.integral_recedingResidual_eq {S K : Set (CKN.Vec 2 × ℝ)} (hS : IsOpen S) (hK : IsCompact K) (hKS : K ⊆ S) {q Fz G divB : CKN.Vec 2 × ℝ → ℝ} {B : CKN.Vec 2 × ℝ → CKN.Vec 2} (κ : ℝ) (hq : ContDiffOn ℝ (↑⊤) q S) (hB : ∀ (i : Fin 2), ContDiffOn ℝ (↑⊤) (fun (z : CKN.Vec 2 × ℝ) => B z i) S) (hF : ContDiffOn ℝ (↑⊤) Fz S) (hG : ContinuousOn G S) (hdiv : ∀ z ∈ S, ∑ i : Fin 2, (fderiv ℝ (fun (w : CKN.Vec 2 × ℝ) => B w i) z) (CKN.basisVec i, 0) = divB z) (hpde : ∀ z ∈ S, (fderiv ℝ q z) (0, 1) + ∑ i : Fin 2, B z i * (fderiv ℝ q z) (CKN.basisVec i, 0) = (∑ i : Fin 2, if ↑i < 1 then (fderiv ℝ (fun (w : CKN.Vec 2 × ℝ) => (fderiv ℝ q w) (CKN.basisVec i, 0)) z) (CKN.basisVec i, 0) else 0) + κ * (fderiv ℝ (fun (w : CKN.Vec 2 × ℝ) => (fderiv ℝ q w) (CKN.basisVec 1, 0)) z) (CKN.basisVec 1, 0) + (fderiv ℝ Fz z) (CKN.basisVec 1, 0) + G z) {ψ : CKN.Vec 2 × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) (hψK : tsupport ψ ⊆ K) : ∫ (z : CKN.Vec 2 × ℝ), q z * (-timeDeriv 2 ψ z - gradPair 2 ψ z (B z) - divB z * ψ z - partialLaplacian 2 1 ψ z) = ∫ (z : CKN.Vec 2 × ℝ), κ * q z * (fderiv ℝ (fun (w : CKN.Vec 2 × ℝ) => (fderiv ℝ ψ w) (CKN.basisVec 1, 0)) z) (CKN.basisVec 1, 0) - Fz z * (fderiv ℝ ψ z) (CKN.basisVec 1, 0) + G z * ψ z

The integration by parts of the receding branch of the passage to the limit: if q, the drift B, the flux Fz and the source G satisfy ∂_τ q + B · ∇q = ∂_RR q + κ ∂_ZZ q + ∂_Z Fz + G pointwise on an open set S, with divB the divergence of B there, then against every test function supported in a compact subset of S the residual of eq:aniso:zoom:receding:limit is κ ∫ q ∂_ZZ ψ - ∫ Fz ∂_Z ψ + ∫ G ψ.

The joint-derivative bridge for dr, dz, dtPast on the plane

theorem CIV.dr_eq_fderiv_apply {F : (ℝ × ℝ) × ℝ → ℝ} {p : (ℝ × ℝ) × ℝ} (hF : DifferentiableAt ℝ F p) : dr F p = (fderiv ℝ F p) ((1, 0), 0)

dr is the joint derivative in the direction ((1, 0), 0).

theorem CIV.dz_eq_fderiv_apply {F : (ℝ × ℝ) × ℝ → ℝ} {p : (ℝ × ℝ) × ℝ} (hF : DifferentiableAt ℝ F p) : dz F p = (fderiv ℝ F p) ((0, 1), 0)

dz is the joint derivative in the direction ((0, 1), 0).

theorem CIV.dtPast_eq_fderiv_apply {F : (ℝ × ℝ) × ℝ → ℝ} {p : (ℝ × ℝ) × ℝ} (hF : DifferentiableAt ℝ F p) : dtPast F p = (fderiv ℝ F p) ((0, 0), 1)

dtPast is the joint derivative in the direction ((0, 0), 1), since a function differentiable at p has equal one-sided and two-sided time derivatives.

theorem CIV.differentiableAt_dr_of_contDiffOn {F : (ℝ × ℝ) × ℝ → ℝ} {D : Set ((ℝ × ℝ) × ℝ)} (hD : IsOpen D) (hF : ContDiffOn ℝ 2 F D) {p : (ℝ × ℝ) × ℝ} (hp : p ∈ D) : DifferentiableAt ℝ (dr F) p

A plane function differentiable on an open set D has a differentiable dr on any set where a further C² bound is known.

theorem CIV.differentiableAt_dz_of_contDiffOn {F : (ℝ × ℝ) × ℝ → ℝ} {D : Set ((ℝ × ℝ) × ℝ)} (hD : IsOpen D) (hF : ContDiffOn ℝ 2 F D) {p : (ℝ × ℝ) × ℝ} (hp : p ∈ D) : DifferentiableAt ℝ (dz F) p

A plane function differentiable on an open set D has a differentiable dz on any set where a further C² bound is known.

def CIV.planeLiftCLM : CKN.Vec 2 × ℝ →L[ℝ] (ℝ × ℝ) × ℝ

The plane-and-time coordinate identification, as a continuous linear map.

Equations

• CIV.planeLiftCLM = ((ContinuousLinearMap.proj 0).prod (ContinuousLinearMap.proj 1) ∘SL ContinuousLinearMap.fst ℝ (CKN.Vec 2) ℝ).prod (ContinuousLinearMap.snd ℝ (CKN.Vec 2) ℝ)

theorem CIV.planeLiftCLM_eq : ⇑planeLiftCLM = planeLiftPoint

theorem CIV.hasFDerivAt_planeLiftPoint (w : CKN.Vec 2 × ℝ) : HasFDerivAt planeLiftPoint planeLiftCLM w

theorem CIV.hasFDerivAt_comp_planeLiftPoint {F : (ℝ × ℝ) × ℝ → ℝ} {w : CKN.Vec 2 × ℝ} (hF : DifferentiableAt ℝ F (planeLiftPoint w)) : HasFDerivAt (fun (w' : CKN.Vec 2 × ℝ) => F (planeLiftPoint w')) (fderiv ℝ F (planeLiftPoint w) ∘SL planeLiftCLM) w

theorem CIV.fderiv_comp_planeLiftPoint_basisVec0 {F : (ℝ × ℝ) × ℝ → ℝ} {w : CKN.Vec 2 × ℝ} (hF : DifferentiableAt ℝ F (planeLiftPoint w)) : (fderiv ℝ (fun (w' : CKN.Vec 2 × ℝ) => F (planeLiftPoint w')) w) (CKN.basisVec 0, 0) = dr F (planeLiftPoint w)

theorem CIV.fderiv_comp_planeLiftPoint_basisVec1 {F : (ℝ × ℝ) × ℝ → ℝ} {w : CKN.Vec 2 × ℝ} (hF : DifferentiableAt ℝ F (planeLiftPoint w)) : (fderiv ℝ (fun (w' : CKN.Vec 2 × ℝ) => F (planeLiftPoint w')) w) (CKN.basisVec 1, 0) = dz F (planeLiftPoint w)

theorem CIV.fderiv_comp_planeLiftPoint_time {F : (ℝ × ℝ) × ℝ → ℝ} {w : CKN.Vec 2 × ℝ} (hF : DifferentiableAt ℝ F (planeLiftPoint w)) : (fderiv ℝ (fun (w' : CKN.Vec 2 × ℝ) => F (planeLiftPoint w')) w) (0, 1) = dtPast F (planeLiftPoint w)

theorem CIV.fderiv_fderiv_comp_planeLiftPoint_basisVec0 {F : (ℝ × ℝ) × ℝ → ℝ} {D : Set ((ℝ × ℝ) × ℝ)} (hD : IsOpen D) (hF : ContDiffOn ℝ 2 F D) {w : CKN.Vec 2 × ℝ} (hw : planeLiftPoint w ∈ D) : (fderiv ℝ (fun (w' : CKN.Vec 2 × ℝ) => (fderiv ℝ (fun (w'' : CKN.Vec 2 × ℝ) => F (planeLiftPoint w'')) w') (CKN.basisVec 0, 0)) w) (CKN.basisVec 0, 0) = dr (dr F) (planeLiftPoint w)

The Vec 2 × ℝ double derivative of a plane function composed with planeLiftPoint, in the direction basisVec 0 twice, in terms of the plane function's own dr ∘ dr.

theorem CIV.fderiv_fderiv_comp_planeLiftPoint_basisVec1 {F : (ℝ × ℝ) × ℝ → ℝ} {D : Set ((ℝ × ℝ) × ℝ)} (hD : IsOpen D) (hF : ContDiffOn ℝ 2 F D) {w : CKN.Vec 2 × ℝ} (hw : planeLiftPoint w ∈ D) : (fderiv ℝ (fun (w' : CKN.Vec 2 × ℝ) => (fderiv ℝ (fun (w'' : CKN.Vec 2 × ℝ) => F (planeLiftPoint w'')) w') (CKN.basisVec 1, 0)) w) (CKN.basisVec 1, 0) = dz (dz F) (planeLiftPoint w)

The Vec 2 × ℝ double derivative of a plane function composed with planeLiftPoint, in the direction basisVec 1 twice, in terms of the plane function's own dz ∘ dz.

The swirl flux and the receding source term

noncomputable def CIV.swirlFluxPlane (lam h rc zc : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (p : (ℝ × ℝ) × ℝ) : ℝ

The receding-axis swirl flux S_n² / (A_n + R) of eq:aniso:zoom:receding:equation.

Equations

• CIV.swirlFluxPlane lam h rc zc u p = CIV.zoomSRec lam h rc zc u p ^ 2 / (rc / lam + p.1.1)

noncomputable def CIV.recedingSourcePlane (lam h rc zc : ℝ) (u f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (p : (ℝ × ℝ) × ℝ) : ℝ

The receding-axis source `(1/(A_n+R))∂_RΘ_n − Θ_n/(A_n+R)² + λ_n⁴δ_n H_n

• (V_n/(A_n+R))Θ_nofeq:aniso:zoom:receding:equation: the four terms that vanish together with the ∂_Z-part of the swirl flux and the δ_n²∂_ZZterm asn → ∞`.

Equations

• One or more equations did not get rendered due to their size.

theorem CIV.dz_swirlFluxPlane_eq (lam h rc zc : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (p : (ℝ × ℝ) × ℝ) : dz (swirlFluxPlane lam h rc zc u) p = 1 / (rc / lam + p.1.1) * dz (fun (q : (ℝ × ℝ) × ℝ) => zoomSRec lam h rc zc u q ^ 2) p

The ∂_Z-derivative of the swirl flux is (1/(A_n+R)) times the ∂_Z-derivative of S_n², since the denominator A_n + R does not depend on Z.

theorem CIV.zoomTheta_pde_source_form {lam h rc zc : ℝ} (hlam : 0 < lam) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {pr : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hsol : IsClassicalSolutionOn u pr f unitCylinder) (haxi : IsAxisymmetricOn u unitCylinder) (p : (ℝ × ℝ) × ℝ) (hp : zoomPointRec lam h rc zc p ∈ unitCylinder) (hR : p.1.1 ≠ -(rc / lam)) : dtPast (zoomTheta lam h rc zc u) p + zoomVRec lam h rc zc u p * dr (zoomTheta lam h rc zc u) p + zoomWRec lam h rc zc u p * dz (zoomTheta lam h rc zc u) p = dr (dr (zoomTheta lam h rc zc u)) p + (lam ^ (2 * h)) ^ 2 * dz (dz (zoomTheta lam h rc zc u)) p + dz (swirlFluxPlane lam h rc zc u) p + recedingSourcePlane lam h rc zc u f p

The rescaled azimuthal vorticity equation of eq:aniso:zoom:receding:equation, rewritten with the transport in advective form and the divergence-free correction, swirl source and force gathered into the swirl flux swirlFluxPlane and the source recedingSourcePlane, ready for integral_recedingResidual_eq.

theorem CIV.continuousOn_dr_of_contDiffOn {F : (ℝ × ℝ) × ℝ → ℝ} {D : Set ((ℝ × ℝ) × ℝ)} (hD : IsOpen D) (hF : ContDiffOn ℝ 2 F D) : ContinuousOn (dr F) D

dr of a plane function ContDiffOn order ≥ 2 on an open set is continuous there.

Domain membership and bounds along the moving centre

R2-R: the residual tends to zero

theorem CIV.tendsto_recResidual {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) (hC : 0 ≤ C) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hb : 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) (φ : CKN.Vec 2 × ℝ → ℝ) : φ ∈ testFunctions 2 (Set.Iio (-1)) → Filter.Tendsto (fun (n : ℕ) => ∫ (z : CKN.Vec 2 × ℝ), zoomTheta (lam n) h (rc n) (zc n) u (planeLiftPoint z) * (-timeDeriv 2 φ z - gradPair 2 φ z (recDrift (lam n) h (rc n) (zc n) u z) - recDriftDiv (lam n) h (rc n) (zc n) u z * φ z - partialLaplacian 2 1 φ z)) Filter.atTop (nhds 0)

R2-R: the residual of the rescaled receding vorticity-quotient equation tends to zero.