CH2.varphi_abs

@[blueprint  "varphi-abs"  (title := "$\\varphi$ absolutely continuous")  (statement := /-- The function $\varphi_\nu^\pm$ is absolutely continuous. -/)  (proof := /-- Apply Lemmas \ref{phi-c2-left}, \ref{phi-c2-right}, \ref{phi-cts} We know $\varphi_\nu^\pm$ is absolutely continuous because it is $C^1$ on $[-1, 0]$ and $[0, 1]$, and identically $0$ outside $[-1, 1]$./-/)  (latexEnv := "lemma")  (discussion := 1226)]theorem varphi_abs (ν ε : ℝ) (hlam : ν ≠ 0) : AbsolutelyContinuous (ϕ_pm ν ε) := by  constructor  · rw [ae_iff]    apply MeasureTheory.measure_mono_null (t := {-1, 0, 1})    · intro x hx      contrapose! hx      simp only [Set.mem_insert_iff, Set.mem_singleton_iff, not_or, Set.mem_setOf_eq, not_not] at hx ⊢      rcases lt_trichotomy x (-1) with h | rfl | h      · exact varphi_differentiableAt_out ν ε (fun hx ↦ (not_le.mpr h) hx.1)      · exfalso; exact hx.1 rfl      · rcases lt_trichotomy x 0 with h' | rfl | h'        · exact varphi_differentiableAt_left ν ε hlam ⟨h, h'⟩        · exfalso; exact hx.2.1 rfl        · rcases lt_trichotomy x 1 with h'' | rfl | h''          · exact varphi_differentiableAt_right ν ε hlam ⟨h', h''⟩          · exfalso; exact hx.2.2 rfl          · exact varphi_differentiableAt_out ν ε (fun hx ↦ (not_le.mpr h'') hx.2)    · apply Set.Finite.measure_zero (by simp)  · intro a b; exact (varphi_ftc ν ε hlam a b).symm