CH2.ϕ_pm_zero_boundary

theorem ϕ_pm_zero_boundary (ν ε : ℝ) (hlam : ν ≠ 0) : ϕ_pm ν ε (-1) = 0 ∧ ϕ_pm ν ε 1 = 0 := by  constructor  · have h_eq : ϕ_pm ν ε =ᶠ[nhdsWithin (-1) (Set.Iio (-1))] 0 := by      filter_upwards [self_mem_nhdsWithin] with z hz      unfold ϕ_pm; split_ifs with hz_mem <;> try rfl      exfalso; linarith [Set.mem_Iio.mp hz]    exact tendsto_nhds_unique      (tendsto_nhdsWithin_of_tendsto_nhds (ϕ_continuous ν ε hlam).continuousAt)      (tendsto_const_nhds.congr' h_eq.symm)  · have h_eq : ϕ_pm ν ε =ᶠ[nhdsWithin 1 (Set.Ioi 1)] 0 := by      filter_upwards [self_mem_nhdsWithin] with z hz      unfold ϕ_pm; split_ifs with hz_mem <;> try rfl      exfalso; linarith [Set.mem_Ioi.mp hz]    exact tendsto_nhds_unique      (tendsto_nhdsWithin_of_tendsto_nhds (ϕ_continuous ν ε hlam).continuousAt)      (tendsto_const_nhds.congr' h_eq.symm)