The raw (uncut) receding zoom slices are smooth on the preimage of unitCylinder

These are the receding-axis analogues of CIV.contDiffOn_zoomV_slice and CIV.contDiffOn_zoomW_slice (CIV/Zoom/FiniteZoomCutoffData.lean). The raw receding zoom slices zoomVRec, zoomWRec at τ = -1 are smooth on the preimage of unitCylinder under the recentred zoom map, since that map is itself smooth (affine) and u is smooth on unitCylinder — together with the pointwise HasFDerivAt facts this openness-and-smoothness combination yields, the same shape as the finite-axis CIV.hasFDerivAt_zoomV_slice_of_mem / CIV.hasFDerivAt_zoomW_slice_of_mem (CIV/Zoom/FiniteZoomCutoffBounds.lean) already use to read off dr/dz as components of the Frechet derivative wherever the raw slice is smooth.

Smoothness of the raw receding zoom slices

theorem CIV.contDiffOn_zoomVRec_slice {h rc zc lam : ℝ} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {pres : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hsol : IsClassicalSolutionOn u pres f unitCylinder) : ContDiffOn ℝ (↑⊤) (fun (q : ℝ × ℝ) => zoomVRec lam h rc zc u (q, -1)) {q : ℝ × ℝ | zoomPointRec lam h rc zc (q, -1) ∈ unitCylinder}

The raw receding radial zoom slice at scale lam is ContDiffOn ℝ (⊤ : ℕ∞) on the preimage of unitCylinder under the recentred zoom map, because it is lam times the zeroth component of u composed with the globally smooth zoomPointRec map, and u itself is smooth wherever the zoom point lands.

theorem CIV.contDiffOn_zoomWRec_slice {h rc zc lam : ℝ} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {pres : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hsol : IsClassicalSolutionOn u pres f unitCylinder) : ContDiffOn ℝ (↑⊤) (fun (q : ℝ × ℝ) => zoomWRec lam h rc zc u (q, -1)) {q : ℝ × ℝ | zoomPointRec lam h rc zc (q, -1) ∈ unitCylinder}

The raw receding vertical zoom slice at scale lam is ContDiffOn ℝ (⊤ : ℕ∞) on the preimage of unitCylinder under the recentred zoom map, because it is lam * lam ^ (2 * h) times the second component of u composed with the globally smooth zoomPointRec map, and u itself is smooth wherever the zoom point lands.

Pointwise HasFDerivAt on the open set where the zoom point is in unitCylinder

theorem CIV.hasFDerivAt_zoomVRec_slice_of_mem {h rc zc lam : ℝ} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {pres : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hsol : IsClassicalSolutionOn u pres f unitCylinder) {y : ℝ × ℝ} (hy : zoomPointRec lam h rc zc (y, -1) ∈ unitCylinder) : HasFDerivAt (fun (q : ℝ × ℝ) => zoomVRec lam h rc zc u (q, -1)) (fderiv ℝ (fun (q : ℝ × ℝ) => zoomVRec lam h rc zc u (q, -1)) y) y

On the preimage of unitCylinder, the Fréchet derivative of the raw receding radial zoom slice is read off dr, dz: it is ContDiffOn there (contDiffOn_zoomVRec_slice), and the preimage is open, so HasFDerivAt holds pointwise and CIV.dr_eq_of_hasFDerivAt / CIV.dz_eq_of_hasFDerivAt apply.

theorem CIV.hasFDerivAt_zoomWRec_slice_of_mem {h rc zc lam : ℝ} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {pres : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hsol : IsClassicalSolutionOn u pres f unitCylinder) {y : ℝ × ℝ} (hy : zoomPointRec lam h rc zc (y, -1) ∈ unitCylinder) : HasFDerivAt (fun (q : ℝ × ℝ) => zoomWRec lam h rc zc u (q, -1)) (fderiv ℝ (fun (q : ℝ × ℝ) => zoomWRec lam h rc zc u (q, -1)) y) y