The second Fréchet derivative of a raw zoom slice, read off nested dr/dz

CIV.step_finite_contradiction needs ‖fderiv ℝ (fderiv ℝ (Vseq n)) y‖ ≤ L. This file supplies the bridge between that operator norm and the pointwise second-order bounds CIV.abs_drdr_zoomV_le_rpow_neg_half etc.: on the open set where a space-time field's time slice is ContDiff ℝ (⊤ : ℕ∞), the three independent entries of its second derivative are exactly dr (dr ·), dr (dz ·), dz (dz ·) evaluated at the frozen time, and the fourth (dz (dr ·)) agrees with dr (dz ·) by symmetry of the second derivative (second_derivative_symmetric) — so no separate bound on it is needed.

HasFDerivAt for a field and its derivative, on an open set

theorem CIV.hasFDerivAt_and_hasFDerivAt_fderiv_of_contDiffOn {g : ℝ × ℝ → ℝ} {S : Set (ℝ × ℝ)} (hS : IsOpen S) (hg : ContDiffOn ℝ (↑⊤) g S) {y : ℝ × ℝ} (hy : y ∈ S) : HasFDerivAt g (fderiv ℝ g y) y ∧ HasFDerivAt (fderiv ℝ g) (fderiv ℝ (fderiv ℝ g) y) y

On an open set where a time slice is ContDiff ℝ (⊤ : ℕ∞), both the slice and its own Fréchet derivative have a HasFDerivAt at every point of the set, reading fderiv at that point as their respective derivatives.

The three independent entries of the second derivative

theorem CIV.fderiv_fderiv_apply_radial_radial_eq_drdr {φ : (ℝ × ℝ) × ℝ → ℝ} {t : ℝ} {S : Set (ℝ × ℝ)} (hS : IsOpen S) (hφ : ContDiffOn ℝ (↑⊤) (fun (q : ℝ × ℝ) => φ (q, t)) S) {y : ℝ × ℝ} (hy : y ∈ S) : ((fderiv ℝ (fderiv ℝ fun (q : ℝ × ℝ) => φ (q, t)) y) (1, 0)) (1, 0) = dr (dr φ) (y, t)

The radial-radial entry of the second derivative of a time slice equals dr (dr φ) at the frozen time.

theorem CIV.fderiv_fderiv_apply_radial_axial_eq_drdz {φ : (ℝ × ℝ) × ℝ → ℝ} {t : ℝ} {S : Set (ℝ × ℝ)} (hS : IsOpen S) (hφ : ContDiffOn ℝ (↑⊤) (fun (q : ℝ × ℝ) => φ (q, t)) S) {y : ℝ × ℝ} (hy : y ∈ S) : ((fderiv ℝ (fderiv ℝ fun (q : ℝ × ℝ) => φ (q, t)) y) (1, 0)) (0, 1) = dr (dz φ) (y, t)

The radial-axial entry of the second derivative of a time slice equals dr (dz φ) at the frozen time.

theorem CIV.fderiv_fderiv_apply_axial_axial_eq_dzdz {φ : (ℝ × ℝ) × ℝ → ℝ} {t : ℝ} {S : Set (ℝ × ℝ)} (hS : IsOpen S) (hφ : ContDiffOn ℝ (↑⊤) (fun (q : ℝ × ℝ) => φ (q, t)) S) {y : ℝ × ℝ} (hy : y ∈ S) : ((fderiv ℝ (fderiv ℝ fun (q : ℝ × ℝ) => φ (q, t)) y) (0, 1)) (0, 1) = dz (dz φ) (y, t)

The axial-axial entry of the second derivative of a time slice equals dz (dz φ) at the frozen time.

theorem CIV.fderiv_fderiv_apply_axial_radial_eq_of_contDiff {g : ℝ × ℝ → ℝ} (hg : ContDiff ℝ (↑⊤) g) (y : ℝ × ℝ) : ((fderiv ℝ (fderiv ℝ g) y) (0, 1)) (1, 0) = ((fderiv ℝ (fderiv ℝ g) y) (1, 0)) (0, 1)

The fourth (axial-radial) entry agrees with the radial-axial one by symmetry of the second derivative of a ContDiff ℝ (⊤ : ℕ∞) function, so it needs no separate bound.