CH2.varphi_ftc_out

lemma varphi_ftc_out (ν ε : ℝ) (hlam : ν ≠ 0) {x y : ℝ}    (h : (x ≤ -1 ∧ y ≤ -1) ∨ (x ≥ 1 ∧ y ≥ 1)) :    ∫ t in x..y, deriv (ϕ_pm ν ε) t = (ϕ_pm ν ε) y - (ϕ_pm ν ε) x := by  let f := ϕ_pm ν ε  change ∫ t in x..y, deriv f t = f y - f x  have hf_const {t : ℝ} (ht : t ≤ -1 ∨ t ≥ 1) : f t = 0 := by    unfold f ϕ_pm; split_ifs with h_mem    · rcases ht with h_le | h_ge      · obtain rfl : t = -1 := by linarith [h_le, h_mem.1]        simpa [ϕ_pm] using (ϕ_pm_zero_boundary ν ε hlam).1      · obtain rfl : t = 1 := by linarith [h_ge, h_mem.2]        simpa [ϕ_pm] using (ϕ_pm_zero_boundary ν ε hlam).2    · rfl  have hf_deriv (t : ℝ) (ht : t < -1 ∨ t > 1) : deriv f t = 0 := by    have h_eq : f =ᶠ[nhds t] (fun _ ↦ (0 : ℂ)) := by      filter_upwards [isClosed_Icc.isOpen_compl.mem_nhds (show t ∉ Set.Icc (-1) 1 from by        intro h; simp only [Set.mem_Icc] at h; rcases ht with ht | ht <;> linarith)] with z hz      unfold f ϕ_pm; exact if_neg hz    exact h_eq.deriv_eq.trans (deriv_const _ _)  rw [hf_const (h.elim (fun h' ↦ Or.inl h'.2) (fun h' ↦ Or.inr h'.2)),      hf_const (h.elim (fun h' ↦ Or.inl h'.1) (fun h' ↦ Or.inr h'.1)), sub_zero]  apply intervalIntegral.integral_zero_ae  rcases h with ⟨hx, hy⟩ | ⟨hx, hy⟩  · have hne_ae : ∀ᵐ (x_1 : ℝ), x_1 ≠ (-1 : ℝ) := by      rw [MeasureTheory.ae_iff, show {x_1 : ℝ | ¬(x_1 ≠ -1)} = {-1} from by ext; simp]      exact Real.volume_singleton    filter_upwards [hne_ae] with x_1 hne    intro hx1    simp only [Set.uIoc, Set.mem_Ioc] at hx1    exact hf_deriv x_1 (Or.inl (lt_of_le_of_ne (le_trans hx1.2 (max_le hx hy)) hne))  · apply Filter.Eventually.of_forall    intro x_1 hx1    simp only [Set.uIoc, Set.mem_Ioc] at hx1    exact hf_deriv x_1 (Or.inr (lt_of_le_of_lt (le_min hx hy) hx1.1))