Lipschitz bounds for ∂_R V_n and for V_n / R up to the axis

Inputs to the admissibility of the lifted drift of eq:drift:Bn:def in Step 2 of the proof of prop:aniso:small. On a rectangle [Ra, Rb] × [Za, Zb] mapped into the unit cylinder at a time τ ≤ -1, the radial derivative ∂_R V_n is Lipschitz with a constant independent of n (eq:aniso:zoom:derivatives at order two; the mixed derivative is taken in either order by the symmetry of the Cartesian mixed partials), and the quotient V_n / R, continued to the axis by ∂_R V_n (the axis value of div_{X,Z} B_n / 2), is Lipschitz on [0, Rb] × [Za, Zb], since V_n vanishes on the axis.

theorem CIV.hasDerivAt_dr_zoomV_radial_slice (lam h zc : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hu : ContDiffOn ℝ 2 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (p : (ℝ × ℝ) × ℝ) (hp : zoomPoint lam h zc p ∈ unitCylinder) : HasDerivAt (fun (r : ℝ) => dr (zoomV lam h zc u) ((r, p.1.2), p.2)) (dr (dr (zoomV lam h zc u)) p) p.1.1

∂_R V_n differentiated in the radial variable along the slice through p.

theorem CIV.hasDerivAt_dr_zoomV_vertical_slice (lam h zc : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (p : (ℝ × ℝ) × ℝ) (hp : zoomPoint lam h zc p ∈ unitCylinder) : HasDerivAt (fun (s : ℝ) => dr (zoomV lam h zc u) ((p.1.1, s), p.2)) (dr (dz (zoomV lam h zc u)) p) p.1.2

∂_R V_n differentiated in the vertical variable along the slice through p; the derivative is ∂_R ∂_Z V_n by the symmetry of the Cartesian mixed partials.

theorem CIV.abs_dr_zoomV_sub_le {C h lam zc Ra Rb Za Zb tau : ℝ} (hlam : 0 < lam) {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) (hC : 0 ≤ C) (hh1 : h ≤ 1 / 2) (htau : tau ≤ -1) (hmem : ∀ y ∈ Set.Icc Ra Rb ×ˢ Set.Icc Za Zb, zoomPoint lam h zc (y, tau) ∈ unitCylinder) {y1 y2 : ℝ × ℝ} (hy1 : y1 ∈ Set.Icc Ra Rb ×ˢ Set.Icc Za Zb) (hy2 : y2 ∈ Set.Icc Ra Rb ×ˢ Set.Icc Za Zb) : |dr (zoomV lam h zc u) (y1, tau) - dr (zoomV lam h zc u) (y2, tau)| ≤ C * (|y1.1 - y2.1| + |y1.2 - y2.2|)

The radial derivative ∂_R V_n is Lipschitz on a rectangle mapped into the cylinder at a time τ ≤ -1: |∂_R V_n(y₁) - ∂_R V_n(y₂)| ≤ C (|R₁ - R₂| + |Z₁ - Z₂|).

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

The quotient V_n / R, continued to the axis by ∂_R V_n.

Equations

• CIV.zoomVQuot lam h zc u p = if p.1.1 = 0 then CIV.dr (CIV.zoomV lam h zc u) p else CIV.zoomV lam h zc u p / p.1.1

theorem CIV.abs_zoomV_sub_mul_dr_le {C h lam zc Rb Za Zb tau : ℝ} (hlam : 0 < lam) {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) (haxi : IsAxisymmetricOn u unitCylinder) (hC : 0 ≤ C) (hh1 : h ≤ 1 / 2) (htau : tau ≤ -1) (hmem : ∀ y ∈ Set.Icc 0 Rb ×ˢ Set.Icc Za Zb, zoomPoint lam h zc (y, tau) ∈ unitCylinder) {R Z : ℝ} (hR : R ∈ Set.Icc 0 Rb) (hZ : Z ∈ Set.Icc Za Zb) : |zoomV lam h zc u ((R, Z), tau) - R * dr (zoomV lam h zc u) ((R, Z), tau)| ≤ C * R ^ 2

The standing hypotheses of this section, for a rectangle [0, Rb] × [Za, Zb].

theorem CIV.abs_zoomVQuot_sub_radial_le {C h lam zc Rb Za Zb tau : ℝ} (hlam : 0 < lam) {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) (haxi : IsAxisymmetricOn u unitCylinder) (hC : 0 ≤ C) (hh1 : h ≤ 1 / 2) (htau : tau ≤ -1) (hmem : ∀ y ∈ Set.Icc 0 Rb ×ˢ Set.Icc Za Zb, zoomPoint lam h zc (y, tau) ∈ unitCylinder) {R1 R2 Z : ℝ} (hR1 : R1 ∈ Set.Icc 0 Rb) (hR2 : R2 ∈ Set.Icc 0 Rb) (hZ : Z ∈ Set.Icc Za Zb) : |zoomVQuot lam h zc u ((R1, Z), tau) - zoomVQuot lam h zc u ((R2, Z), tau)| ≤ 2 * C * |R1 - R2|

The quotient is Lipschitz along a radial slice through [0, Rb], with constant 2C.

theorem CIV.abs_zoomVQuot_sub_vertical_le {C h lam zc Rb Za Zb tau : ℝ} (hlam : 0 < lam) {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) (haxi : IsAxisymmetricOn u unitCylinder) (hC : 0 ≤ C) (hh1 : h ≤ 1 / 2) (htau : tau ≤ -1) (hmem : ∀ y ∈ Set.Icc 0 Rb ×ˢ Set.Icc Za Zb, zoomPoint lam h zc (y, tau) ∈ unitCylinder) {R Z1 Z2 : ℝ} (hR : R ∈ Set.Icc 0 Rb) (hZ1 : Z1 ∈ Set.Icc Za Zb) (hZ2 : Z2 ∈ Set.Icc Za Zb) : |zoomVQuot lam h zc u ((R, Z1), tau) - zoomVQuot lam h zc u ((R, Z2), tau)| ≤ C * |Z1 - Z2|

The quotient is Lipschitz along a vertical slice, with constant C.

theorem CIV.abs_zoomVQuot_sub_le {C h lam zc Rb Za Zb tau : ℝ} (hlam : 0 < lam) {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) (haxi : IsAxisymmetricOn u unitCylinder) (hC : 0 ≤ C) (hh1 : h ≤ 1 / 2) (htau : tau ≤ -1) (hmem : ∀ y ∈ Set.Icc 0 Rb ×ˢ Set.Icc Za Zb, zoomPoint lam h zc (y, tau) ∈ unitCylinder) {y1 y2 : ℝ × ℝ} (hy1 : y1 ∈ Set.Icc 0 Rb ×ˢ Set.Icc Za Zb) (hy2 : y2 ∈ Set.Icc 0 Rb ×ˢ Set.Icc Za Zb) : |zoomVQuot lam h zc u (y1, tau) - zoomVQuot lam h zc u (y2, tau)| ≤ 2 * C * (|y1.1 - y2.1| + |y1.2 - y2.2|)

The quotient is Lipschitz on the rectangle [0, Rb] × [Za, Zb], with constant 2C for the sum of the coordinate increments.