Bridge from dtPast to HasDerivAt

dtPast is defined in CIV.Statements.DtPast as a derivWithin over Set.Iic — Mathlib's junk-value-on-non-differentiability one-sided derivative. These lemmas bridge that identity to a genuine HasDerivAt of the time-slice, so that a dtPast-shaped identity from a zoom PDE (CIV.zoomTheta_pde, CIV.zoomOmega_pde) can certify a derivative once differentiability in time is separately known, feeding differentiation under the integral sign toward the equation-based time-pairing estimate hpair.

theorem CIV.dtPast_eq_of_hasDerivAt {phi : (ℝ × ℝ) × ℝ → ℝ} {p : (ℝ × ℝ) × ℝ} {v : ℝ} (h : HasDerivAt (fun (t : ℝ) => phi (p.1, t)) v p.2) : dtPast phi p = v

theorem CIV.hasDerivAt_of_dtPast_eq {phi : (ℝ × ℝ) × ℝ → ℝ} {p : (ℝ × ℝ) × ℝ} {v : ℝ} (hdiff : DifferentiableAt ℝ (fun (t : ℝ) => phi (p.1, t)) p.2) (heq : dtPast phi p = v) : HasDerivAt (fun (t : ℝ) => phi (p.1, t)) v p.2

theorem CIV.hasDerivAt_iff_dtPast_eq {phi : (ℝ × ℝ) × ℝ → ℝ} {p : (ℝ × ℝ) × ℝ} {v : ℝ} (hdiff : DifferentiableAt ℝ (fun (t : ℝ) => phi (p.1, t)) p.2) : HasDerivAt (fun (t : ℝ) => phi (p.1, t)) v p.2 ↔ dtPast phi p = v