CH2.varphi_deriv_tv

@[blueprint  "varphi-deriv-tv"  (title := "$\\varphi'$ total variation")  (statement := /-- The function $(\varphi_\nu^\pm)'$ has finite total variation. -/)  (proof := /-- Since $(\varphi_\nu^\pm)'$ is $C^1$ on $[-1, 0]$ and on $[0, 1]$, the $L^1$ norm of $(\varphi_\nu^\pm)''$ on each of these intervals is finite, and so $(\varphi_\nu^\pm)'$ has finite total variation on each of them. As $(\varphi_\nu^\pm)'$ has right and left limits at $-1$, $0$ and $1$, the jumps at those points are finite, and so their contribution to $\|(\varphi_\nu^\pm)'\|_{\mathrm{TV}}$ is finite./-/)  (latexEnv := "lemma")  (discussion := 1229)]theorem varphi_deriv_tv (ν ε : ℝ) (hlam : ν ≠ 0) : BoundedVariationOn (deriv (ϕ_pm ν ε)) Set.univ := by  set g := deriv (ϕ_pm ν ε)  have hBV_left := varphi_deriv_bv_on_Icc ν ε (a := -1) (b := 0) (m := -1/2)    (by norm_num) (by norm_num) (by norm_num) (ϕ_c2_left ν ε hlam)  have hBV_right := varphi_deriv_bv_on_Icc ν ε (a := 0) (b := 1) (m := 1/2)    (by norm_num) (by norm_num) (by norm_num) (ϕ_c2_right ν ε hlam)  have hBV_Icc : BoundedVariationOn g (Set.Icc (-1 : ℝ) 1) := by    simp only [BoundedVariationOn] at hBV_left hBV_right ⊢    have h_split : eVariationOn g (Set.Icc (-1 : ℝ) 0) + eVariationOn g (Set.Icc 0 1) =        eVariationOn g (Set.Icc (-1 : ℝ) 1) := by      simpa only [Set.univ_inter] using eVariationOn.Icc_add_Icc g (by norm_num) (by norm_num) (Set.mem_univ _)    rw [← h_split]    exact ENNReal.add_ne_top.mpr ⟨hBV_left, hBV_right⟩  simp only [BoundedVariationOn] at hBV_Icc ⊢  have h_split1 : eVariationOn g Set.univ =      eVariationOn g (Set.Iic (-1 : ℝ)) + eVariationOn g (Set.Ici (-1 : ℝ)) := by    conv_lhs => rw [← Set.Iic_union_Ici (a := (-1 : ℝ))]    exact eVariationOn.union g isGreatest_Iic isLeast_Ici  have h_split2 : eVariationOn g (Set.Ici (-1 : ℝ)) =      eVariationOn g (Set.Icc (-1 : ℝ) 1) + eVariationOn g (Set.Ici (1 : ℝ)) := by    conv_lhs => rw [← Set.Icc_union_Ici_eq_Ici (by norm_num : (-1 : ℝ) ≤ 1)]    exact eVariationOn.union g (isGreatest_Icc (by norm_num)) isLeast_Ici  rw [h_split1, h_split2]  exact ENNReal.add_ne_top.mpr    ⟨ϕ_pm_deriv_Iic_finite ν ε, ENNReal.add_ne_top.mpr ⟨hBV_Icc, ϕ_pm_deriv_Ici_finite ν ε⟩⟩