CH2.varphi_deriv_integ

@[blueprint  "varphi-deriv-integ"  (title := "$\\varphi'$ integrable")  (statement := /-- The function $(\varphi_\nu^\pm)'$ is integrable. -/)  (proof := /-- Apply Lemmas \ref{phi-c2-left}, \ref{phi-c2-right}, \ref{phi-cts} We know $(\varphi_\nu^\pm)'$ is integrable because it is $C^1$ on $[-1, 0]$ and $[0, 1]$, and identically $0$ outside $[-1, 1]$./-/)  (latexEnv := "lemma")  (discussion := 1228)]theorem varphi_deriv_integ (ν ε : ℝ) (hlam : ν ≠ 0) : Integrable (deriv (ϕ_pm ν ε)) := by  rw [← integrableOn_univ, ← Set.union_compl_self (Set.Icc (-1 : ℝ) 1)]  refine IntegrableOn.union ?_ ?_  · rw [(Set.Icc_union_Icc_eq_Icc (by norm_num : (-1:ℝ) ≤ 0) (by norm_num : (0:ℝ) ≤ 1)).symm]    exact (contDiffOn_Icc_deriv_integrableOn (by norm_num) (ϕ_c2_left ν ε hlam)).union      (contDiffOn_Icc_deriv_integrableOn (by norm_num) (ϕ_c2_right ν ε hlam))  · exact (integrable_zero ℝ ℂ volume).integrableOn.congr_fun (by      intro t ht      have h_eq : ϕ_pm ν ε =ᶠ[nhds t] (fun _ ↦ (0 : ℂ)) := by        filter_upwards [isClosed_Icc.isOpen_compl.mem_nhds ht] with x hx        unfold ϕ_pm; exact if_neg hx      exact (h_eq.deriv_eq.trans (deriv_const _ _)).symm) measurableSet_Icc.compl