support_ψ

lemma support_ψ : support (ψ D) = Ioo (4 * D : ℝ)⁻¹ 2⁻¹ := by  ext x  by_cases! hx₀ : x ≤ 1 / (4 * D)  · suffices x ≤ (D : ℝ)⁻¹ * 4⁻¹ by simp [ψ_formula₀ hx₀, this]    rwa [one_div, mul_inv_rev] at hx₀  have hx₀_inv : (D : ℝ)⁻¹ * 4⁻¹ < x := by convert! hx₀ using 1; simp  have ne₀ : 4 * D * x - 1 ≠ 0 := ne_of_gt (by rwa [sub_pos, ← div_lt_iff₀' (by linarith)])  by_cases! hx₁ : x ≤ 1 / (2 * D)  · suffices (D : ℝ)⁻¹ * 4⁻¹ < x ∧ x < 2⁻¹ by simpa [ne₀, ψ_formula₁ hD ⟨hx₀.le, hx₁⟩]    exact ⟨hx₀_inv, lt_of_le_of_lt hx₁ (by simp [_root_.inv_lt_one_iff₀, hD])⟩  by_cases! hx₂ : x ≤ 1 / 4  · simpa [ψ_formula₂ hD ⟨hx₁.le, hx₂⟩, hx₀_inv] using lt_of_le_of_lt hx₂ (by norm_num)  by_cases hx₃ : x < 1 / 2  · have : ¬ 2 - 4 * x = 0 := by linarith    simpa [ψ_formula₃ hD ⟨hx₂.le, hx₃.le⟩, hx₀, hx₃, ← one_div]  · rw [mem_support, ψ_formula₄ (not_lt.1 hx₃), ne_self_iff_false, false_iff, mem_Ioo, not_and,      inv_eq_one_div 2]    exact fun _ ↦ hx₃