BKLNW_app.μ_antitoneOn

lemma μ_antitoneOn {c ε : ℝ} (hc : 0 < c) (hε : 0 < ε) :    AntitoneOn (μ c ε) (Set.Ioi 0) := by  intro s hs t ht hst  rw [Set.mem_Ioi] at hs ht  unfold μ  rw [if_neg (by linarith : ¬ t < 0), if_pos ht, if_neg (by linarith : ¬ s < 0),    if_pos hs, pre_μ, pre_μ, neg_neg, neg_neg]  refine MeasureTheory.setIntegral_mono_set ((integrable_η hc hε).integrableOn)    (MeasureTheory.ae_of_all _ fun ξ ↦ η_nonneg hc hε ξ) ?_  exact (Set.Iic_subset_Iic.mpr (by linarith : -t ≤ -s)).eventuallyLE