CH2.varphi_ftc

lemma varphi_ftc (ν ε : ℝ) (hlam : ν ≠ 0) (a b : ℝ) :    ∫ t in a..b, deriv (ϕ_pm ν ε) t = (ϕ_pm ν ε) b - (ϕ_pm ν ε) a := by  let f := ϕ_pm ν ε  have h_int x y : IntervalIntegrable (deriv f) volume x y := (varphi_deriv_integ ν ε hlam).intervalIntegrable  wlog h : a ≤ b generalizing a b; · rw [intervalIntegral.integral_symm, this b a (by linarith)]; ring  rw [← intervalIntegral.integral_add_adjacent_intervals (h_int a (-1)) (h_int (-1) b),      ← intervalIntegral.integral_add_adjacent_intervals (h_int (-1) 0) (h_int 0 b),      ← intervalIntegral.integral_add_adjacent_intervals (h_int 0 1) (h_int 1 b),      varphi_ftc_left ν ε hlam ⟨le_refl _, by norm_num⟩ ⟨by norm_num, le_refl _⟩,      varphi_ftc_right ν ε hlam ⟨le_refl _, by norm_num⟩ ⟨by norm_num, le_refl _⟩]  have hL p : ∫ t in p..(-1), deriv f t = f (-1) - f p := by    rcases le_or_gt p (-1) with h_le | h_gt    · exact varphi_ftc_out ν ε hlam (Or.inl ⟨h_le, le_refl _⟩)    · rw [← intervalIntegral.integral_add_adjacent_intervals (h_int p 0) (h_int 0 (-1))]      rcases le_or_gt p 0 with hp0 | hp0      · rw [varphi_ftc_left ν ε hlam ⟨h_gt.le, hp0⟩ ⟨by norm_num, le_refl _⟩,            varphi_ftc_left ν ε hlam ⟨by norm_num, le_refl _⟩ ⟨le_refl _, by norm_num⟩]; ring      · rw [← intervalIntegral.integral_add_adjacent_intervals (h_int p 1) (h_int 1 0)]        rcases le_or_gt p 1 with hp1 | hp1        · rw [varphi_ftc_right ν ε hlam ⟨hp0.le, hp1⟩ ⟨by norm_num, le_refl _⟩,              varphi_ftc_right ν ε hlam ⟨by norm_num, le_refl _⟩ ⟨le_refl _, by norm_num⟩,              varphi_ftc_left ν ε hlam ⟨by norm_num, le_refl _⟩ ⟨le_refl _, by norm_num⟩]; ring        · rw [varphi_ftc_out ν ε hlam (Or.inr ⟨hp1.le, le_refl _⟩),              varphi_ftc_right ν ε hlam ⟨by norm_num, le_refl _⟩ ⟨le_refl _, by norm_num⟩,              varphi_ftc_left ν ε hlam ⟨by norm_num, le_refl _⟩ ⟨le_refl _, by norm_num⟩]; ring  have hR p : ∫ t in 1..p, deriv f t = f p - f 1 := by    rcases le_or_gt p 1 with h_le | h_gt    · rw [← intervalIntegral.integral_add_adjacent_intervals (h_int 1 0) (h_int 0 p)]      rcases le_or_gt p 0 with hp0 | hp0      · rw [← intervalIntegral.integral_add_adjacent_intervals (h_int 0 (-1)) (h_int (-1) p)]        rcases le_or_gt p (-1) with hp_1 | hp_1        · rw [varphi_ftc_right ν ε hlam ⟨by norm_num, le_refl _⟩ ⟨le_refl _, by norm_num⟩,              varphi_ftc_left ν ε hlam ⟨by norm_num, le_refl _⟩ ⟨le_refl _, by norm_num⟩,              varphi_ftc_out ν ε hlam (Or.inl ⟨le_refl _, hp_1⟩)]; ring        · rw [varphi_ftc_right ν ε hlam ⟨by norm_num, le_refl _⟩ ⟨le_refl _, by norm_num⟩,              varphi_ftc_left ν ε hlam ⟨by norm_num, le_refl _⟩ ⟨le_refl _, by norm_num⟩,              varphi_ftc_left ν ε hlam ⟨le_refl _, by norm_num⟩ ⟨hp_1.le, hp0⟩]; ring      · rw [varphi_ftc_right ν ε hlam ⟨by norm_num, le_refl _⟩ ⟨le_refl _, by norm_num⟩,            varphi_ftc_right ν ε hlam ⟨le_refl _, by norm_num⟩ ⟨hp0.le, h_le⟩]; ring    · exact varphi_ftc_out ν ε hlam (Or.inr ⟨le_refl _, h_gt.le⟩)  rw [hL a, hR b]; ring