Rescaled anisotropic bounds (eq:aniso:zoom:derivatives)

The anisotropic Type II bounds eq:aniso:bounds are invariant under the zoom-in map eq:aniso:zoom:finite:variables: the rescaled fields zoomV, zoomW, zoomS of eq:aniso:zoom:fields obey the same bounds, with the same constant C, in the rescaled parabolic time p.2.

Each of the twelve statements below is an instantiation of one of the two private scale-invariance lemmas: the derivative is rewritten by the chain rules of CIV.Zoom.ChainRule / CIV.Zoom.ChainRuleSecond, AnisotropicBounds is applied at the zoomed point zoomPoint lam h zc p, whose parabolic time is lam ^ 2 * p.2, and the lam prefactors are cancelled against that lam ^ 2 by zoom_rescaled_exponent (radial component) or zoom_rescaled_exponent_swirl (vertical and swirl components).

theorem CIV.abs_zoomV_le (C h lam zc : ℝ) (hlam : 0 < lam) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hb : AnisotropicBounds C h u) (p : (ℝ × ℝ) × ℝ) (hp : zoomPoint lam h zc p ∈ unitCylinder) : |zoomV lam h zc u p| ≤ C * (-p.2) ^ (-(1 / 2) - 0 / 2 - (1 / 2 - h) * 0)

theorem CIV.abs_dr_zoomV_le (C h lam zc : ℝ) (hlam : 0 < lam) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hb : AnisotropicBounds C h u) (hu : ContDiffOn ℝ 2 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (p : (ℝ × ℝ) × ℝ) (hp : zoomPoint lam h zc p ∈ unitCylinder) : |dr (zoomV lam h zc u) p| ≤ C * (-p.2) ^ (-(1 / 2) - 1 / 2 - (1 / 2 - h) * 0)

theorem CIV.abs_dz_zoomV_le (C h lam zc : ℝ) (hlam : 0 < lam) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hb : AnisotropicBounds C h u) (hu : ContDiffOn ℝ 2 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (p : (ℝ × ℝ) × ℝ) (hp : zoomPoint lam h zc p ∈ unitCylinder) : |dz (zoomV lam h zc u) p| ≤ C * (-p.2) ^ (-(1 / 2) - 0 / 2 - (1 / 2 - h) * 1)

theorem CIV.abs_drdr_zoomV_le (C h lam zc : ℝ) (hlam : 0 < lam) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hb : AnisotropicBounds C h u) (hu : ContDiffOn ℝ 2 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (p : (ℝ × ℝ) × ℝ) (hp : zoomPoint lam h zc p ∈ unitCylinder) : |dr (dr (zoomV lam h zc u)) p| ≤ C * (-p.2) ^ (-(1 / 2) - 2 / 2 - (1 / 2 - h) * 0)

theorem CIV.abs_drdz_zoomV_le (C h lam zc : ℝ) (hlam : 0 < lam) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hb : AnisotropicBounds C h u) (hu : ContDiffOn ℝ 2 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (p : (ℝ × ℝ) × ℝ) (hp : zoomPoint lam h zc p ∈ unitCylinder) : |dr (dz (zoomV lam h zc u)) p| ≤ C * (-p.2) ^ (-(1 / 2) - 1 / 2 - (1 / 2 - h) * 1)

theorem CIV.abs_dzdz_zoomV_le (C h lam zc : ℝ) (hlam : 0 < lam) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hb : AnisotropicBounds C h u) (hu : ContDiffOn ℝ 2 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (p : (ℝ × ℝ) × ℝ) (hp : zoomPoint lam h zc p ∈ unitCylinder) : |dz (dz (zoomV lam h zc u)) p| ≤ C * (-p.2) ^ (-(1 / 2) - 0 / 2 - (1 / 2 - h) * 2)

theorem CIV.abs_zoomW_add_abs_zoomS_le (C h lam zc : ℝ) (hlam : 0 < lam) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hb : AnisotropicBounds C h u) (p : (ℝ × ℝ) × ℝ) (hp : zoomPoint lam h zc p ∈ unitCylinder) : |zoomW lam h zc u p| + |zoomS lam h zc u p| ≤ C * (-p.2) ^ (-(1 / 2) - h - 0 / 2 - (1 / 2 - h) * 0)

theorem CIV.abs_dr_zoomW_add_abs_dr_zoomS_le (C h lam zc : ℝ) (hlam : 0 < lam) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hb : AnisotropicBounds C h u) (hu : ContDiffOn ℝ 2 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (p : (ℝ × ℝ) × ℝ) (hp : zoomPoint lam h zc p ∈ unitCylinder) : |dr (zoomW lam h zc u) p| + |dr (zoomS lam h zc u) p| ≤ C * (-p.2) ^ (-(1 / 2) - h - 1 / 2 - (1 / 2 - h) * 0)

theorem CIV.abs_dz_zoomW_add_abs_dz_zoomS_le (C h lam zc : ℝ) (hlam : 0 < lam) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hb : AnisotropicBounds C h u) (hu : ContDiffOn ℝ 2 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (p : (ℝ × ℝ) × ℝ) (hp : zoomPoint lam h zc p ∈ unitCylinder) : |dz (zoomW lam h zc u) p| + |dz (zoomS lam h zc u) p| ≤ C * (-p.2) ^ (-(1 / 2) - h - 0 / 2 - (1 / 2 - h) * 1)

theorem CIV.abs_drdr_zoomW_add_abs_drdr_zoomS_le (C h lam zc : ℝ) (hlam : 0 < lam) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hb : AnisotropicBounds C h u) (hu : ContDiffOn ℝ 2 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (p : (ℝ × ℝ) × ℝ) (hp : zoomPoint lam h zc p ∈ unitCylinder) : |dr (dr (zoomW lam h zc u)) p| + |dr (dr (zoomS lam h zc u)) p| ≤ C * (-p.2) ^ (-(1 / 2) - h - 2 / 2 - (1 / 2 - h) * 0)

theorem CIV.abs_drdz_zoomW_add_abs_drdz_zoomS_le (C h lam zc : ℝ) (hlam : 0 < lam) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hb : AnisotropicBounds C h u) (hu : ContDiffOn ℝ 2 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (p : (ℝ × ℝ) × ℝ) (hp : zoomPoint lam h zc p ∈ unitCylinder) : |dr (dz (zoomW lam h zc u)) p| + |dr (dz (zoomS lam h zc u)) p| ≤ C * (-p.2) ^ (-(1 / 2) - h - 1 / 2 - (1 / 2 - h) * 1)

theorem CIV.abs_dzdz_zoomW_add_abs_dzdz_zoomS_le (C h lam zc : ℝ) (hlam : 0 < lam) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hb : AnisotropicBounds C h u) (hu : ContDiffOn ℝ 2 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (p : (ℝ × ℝ) × ℝ) (hp : zoomPoint lam h zc p ∈ unitCylinder) : |dz (dz (zoomW lam h zc u)) p| + |dz (dz (zoomS lam h zc u)) p| ≤ C * (-p.2) ^ (-(1 / 2) - h - 0 / 2 - (1 / 2 - h) * 2)