interval_approx_inf

lemma interval_approx_inf (ha : 0 < a) (hab : a < b) :    ∀ᶠ ε in 𝓝[>] 0, ∃ ψ : ℝ → ℝ, ContDiff ℝ ∞ ψ ∧ HasCompactSupport ψ ∧      closure (Function.support ψ) ⊆ Set.Ioi 0 ∧        ψ ≤ indicator (Ico a b) 1 ∧ b - a - ε ≤ ∫ y in Ioi 0, ψ y := by   have l1 : Iio ((b - a) / 3) ∈ 𝓝[>] 0 := nhdsWithin_le_nhds <| Iio_mem_nhds <| by    rw [← sub_pos] at hab    positivity  filter_upwards [self_mem_nhdsWithin, l1] with ε (hε : 0 < ε) (hε' : ε < (b - a) / 3)  have l2 : a < a + ε / 2 := by simp [hε]  have l3 : b - ε / 2 < b := by simp [hε]  obtain ⟨ψ, h1, h2, h3, h4, h5⟩ := smooth_urysohn_support_Ioo l2 l3  refine ⟨ψ, h1, h2, ?_, ?_, ?_⟩  · simp [h5, hab.ne, Icc_subset_Ioi_iff hab.le, ha]  · exact h4.trans <| indicator_le_indicator_of_subset Ioo_subset_Ico_self (by simp)  · have l4 : 0 ≤ b - a - ε := by linarith    have l5 : Icc (a + ε / 2) (b - ε / 2) ⊆ Ioi 0 := by      intro t ht      simp only [mem_Icc, mem_Ioi] at ht ⊢      exact ha.trans <| l2.trans_le <| ht.1    have l6 : Icc (a + ε / 2) (b - ε / 2) ∩ Ioi 0 = Icc (a + ε / 2) (b - ε / 2) :=      inter_eq_left.mpr l5    have l7 : ∫ y in Ioi 0, indicator (Icc (a + ε / 2) (b - ε / 2)) 1 y = b - a - ε := by      simp only [measurableSet_Icc, integral_indicator_one, measureReal_restrict_apply, l6,        volume_real_Icc]      convert max_eq_left l4 using 1 ; ring_nf    have l8 : IntegrableOn ψ (Ioi 0) volume :=      (h1.continuous.integrable_of_hasCompactSupport h2).integrableOn    rw [← l7] ; apply setIntegral_mono ?_ l8 h3    rw [IntegrableOn, integrable_indicator_iff measurableSet_Icc]    apply IntegrableOn.mono ?_ subset_rfl Measure.restrict_le_self    apply integrableOn_const <;>    simp