Cusp-Approaching Path Continuity

Helpers for cusp-approaching paths, specifically continuity of φ₀ along paths approaching i∞.

Main results

• continuousOn_φ₀''_cusp_path: t ↦ φ₀''(-1/(I*t)) is continuous on (0, ∞)

theorem continuousOn_φ₀''_cusp_path : ContinuousOn (fun (t : ℝ) => φ₀'' (-1 / (Complex.I * ↑t))) (Set.Ioi 0)

ContinuousOn for the cusp-approaching path: t ↦ φ₀''(-1/(It)) is continuous on (0, ∞). Since -1/(It) = I/t and Im(I/t) = 1/t > 0 for t > 0, this factors through φ₀_continuous.