hVbdd/hWbdd: value and first-derivative operator-norm bounds on growing squares

For every fixed j, once n is large enough that the cutoff equals 1 throughout halfPlaneRectangle (j + 1), the cutoff-multiplied field coincides there with the raw zoom slice, together with its Fréchet derivative — so the uniform, n-independent pointwise bounds of CIV.VBoundedRectangle and CIV.RescaledBounds transfer directly, through the dual-norm bound of CIV.OperatorNormProd.

Local agreement, as functions, on an open ball around a rectangle

theorem CIV.norm_le_of_mem_halfPlaneRectangle {j : ℕ} {y : ℝ × ℝ} (hy : y ∈ halfPlaneRectangle j) : ‖y‖ ≤ ↑j + 1

Every point of halfPlaneRectangle j has sup norm at most j + 1.

theorem CIV.eventually_forall_mem_halfPlaneRectangle_cutoffZoomV_eq {h : ℝ} (hh1 : h < 1 / 2) {zc : ℕ → ℝ} {ζ : ℝ} (hzc : ∀ (n : ℕ), |zc n| ≤ ζ) (hζ : ζ < 1) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {lam : ℕ → ℝ} (hlam0 : ∀ (n : ℕ), 0 < lam n) (hlamTendsto : Filter.Tendsto lam Filter.atTop (nhds 0)) (j : ℕ) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ y ∈ halfPlaneRectangle j, cutoffZoomV h zc hzc hζ u lam hlam0 n y = zoomV (lam n) h (zc n) u (y, -1) ∧ fderiv ℝ (cutoffZoomV h zc hzc hζ u lam hlam0 n) y = fderiv ℝ (fun (q : ℝ × ℝ) => zoomV (lam n) h (zc n) u (q, -1)) y

Once n is large enough, the cutoff-multiplied radial field agrees with the raw zoom slice, together with its Fréchet derivative, throughout halfPlaneRectangle j.

theorem CIV.eventually_forall_mem_halfPlaneRectangle_cutoffZoomW_eq {h : ℝ} (hh1 : h < 1 / 2) {zc : ℕ → ℝ} {ζ : ℝ} (hzc : ∀ (n : ℕ), |zc n| ≤ ζ) (hζ : ζ < 1) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {lam : ℕ → ℝ} (hlam0 : ∀ (n : ℕ), 0 < lam n) (hlamTendsto : Filter.Tendsto lam Filter.atTop (nhds 0)) (j : ℕ) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ y ∈ halfPlaneRectangle j, cutoffZoomW h zc hzc hζ u lam hlam0 n y = zoomW (lam n) h (zc n) u (y, -1) ∧ fderiv ℝ (cutoffZoomW h zc hzc hζ u lam hlam0 n) y = fderiv ℝ (fun (q : ℝ × ℝ) => zoomW (lam n) h (zc n) u (q, -1)) y

The vertical counterpart of eventually_forall_mem_halfPlaneRectangle_cutoffZoomV_eq.

The Fréchet derivative of the raw slice, read off dr/dz, wherever it is smooth

theorem CIV.hasFDerivAt_zoomV_slice_of_mem {h 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 : zoomPoint lam h zc (y, -1) ∈ unitCylinder) : HasFDerivAt (fun (q : ℝ × ℝ) => zoomV lam h zc u (q, -1)) (fderiv ℝ (fun (q : ℝ × ℝ) => zoomV lam h zc u (q, -1)) y) y

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

theorem CIV.hasFDerivAt_zoomW_slice_of_mem {h 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 : zoomPoint lam h zc (y, -1) ∈ unitCylinder) : HasFDerivAt (fun (q : ℝ × ℝ) => zoomW lam h zc u (q, -1)) (fderiv ℝ (fun (q : ℝ × ℝ) => zoomW lam h zc u (q, -1)) y) y

Uniform value and first-derivative bounds on the raw slices

theorem CIV.abs_zoomV_slice_le {C h zc lam : ℝ} (hlam : 0 < lam) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hb : AnisotropicBounds C h u) {y : ℝ × ℝ} (hy : zoomPoint lam h zc (y, -1) ∈ unitCylinder) : |zoomV lam h zc u (y, -1)| ≤ C

The uniform (lam-independent) value bound on the raw radial zoom slice at the frozen time τ = -1.

theorem CIV.abs_zoomW_slice_le {C h zc lam : ℝ} (hlam : 0 < lam) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hb : AnisotropicBounds C h u) {y : ℝ × ℝ} (hy : zoomPoint lam h zc (y, -1) ∈ unitCylinder) : |zoomW lam h zc u (y, -1)| ≤ C

The uniform value bound on the raw vertical zoom slice, dropping the swirl term.

theorem CIV.norm_fderiv_zoomV_slice_le {C h zc lam : ℝ} (hlam : 0 < lam) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hb : AnisotropicBounds C h u) {pres : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hsol : IsClassicalSolutionOn u pres f unitCylinder) {y : ℝ × ℝ} (hy : zoomPoint lam h zc (y, -1) ∈ unitCylinder) : ‖fderiv ℝ (fun (q : ℝ × ℝ) => zoomV lam h zc u (q, -1)) y‖ ≤ 2 * C

The uniform operator-norm bound on the Fréchet derivative of the raw radial zoom slice.

theorem CIV.norm_fderiv_zoomW_slice_le {C h zc lam : ℝ} (hlam : 0 < lam) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hb : AnisotropicBounds C h u) {pres : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hsol : IsClassicalSolutionOn u pres f unitCylinder) {y : ℝ × ℝ} (hy : zoomPoint lam h zc (y, -1) ∈ unitCylinder) : ‖fderiv ℝ (fun (q : ℝ × ℝ) => zoomW lam h zc u (q, -1)) y‖ ≤ 2 * C

The uniform operator-norm bound on the Fréchet derivative of the raw vertical zoom slice.