CH2.ϕ_c2_right

@[blueprint  "phi-c2-right"  (title := "$\\varphi$ is $C^2$ on [0,1]")  (statement := /--  $\varphi$ is $C^2$ on $[0,1]$.  -/)  (proof := /-- Since $\Phi^{\pm, \circ}_\nu(z)$ and $\Phi^{\pm, \circ}_\nu(z)$ have no poles on $\mathbb{R}$, they have no poles on some open neighborhood of $[-1,1]$. Hence they are $C^2$ on this interval.  Since $w(0) = \nu$, we see that $\Phi^{\pm, \ast}_\nu(0)=0$, giving the claim. -/)  (latexEnv := "lemma")]theorem ϕ_c2_right (ν ε : ℝ) (hlam : ν ≠ 0) : ContDiffOn ℝ 2 (ϕ_pm ν ε) (Set.Icc 0 1) := by  have hs : ContDiffOn ℝ 2 (fun t : ℝ => Phi_star ν ε (t : ℂ)) (Set.Icc 0 1) :=    (Phi_star.contDiff_real ν ε hlam).contDiffOn  have hcirc : ContDiffOn ℝ 2 (fun t : ℝ => Phi_circ ν ε (t : ℂ)) (Set.Icc 0 1) := (Phi_circ.contDiff_real ν ε hlam).contDiffOn  exact (hcirc.add hs).congr fun t ht => by    simp only [ϕ_pm]    rw [if_pos ⟨by linarith [ht.1], ht.2⟩]    rcases eq_or_lt_of_le ht.1 with rfl | hpos    · simp [Real.sign_zero, Phi_star_zero]    · simp [Real.sign_of_pos hpos]