feat(Topology/Order/IsLUB): introduce lemmas for rewriting inequalities under CountableInterFilter (leanprover-community#34375)

Introduce the following lemmas:

- eventually_le_const_iff_forall_gt_eventually_lt_const
- eventually_const_le_iff_forall_lt_eventually_const_lt

which can be used to get an epsilon of room outside the filter in an eventual inequality. As an application, proofs of some lemmas for `limsup` and `ae` inequalities are simplified.

Author: jvanwinden

Mathlib/MeasureTheory/Function/AEEqOfLIntegral.lean

@@ -42,35 +42,7 @@ variable {α : Type*} {m m0 : MeasurableSpace α} {μ : Measure α} {p : ℝ≥0
 theorem ae_const_le_iff_forall_lt_measure_zero {β} [LinearOrder β] [TopologicalSpace β]
     [OrderTopology β] [FirstCountableTopology β] (f : α → β) (c : β) :
     (∀ᵐ x ∂μ, c ≤ f x) ↔ ∀ b < c, μ {x | f x ≤ b} = 0 := by
-  rw [ae_iff]
-  push Not
-  constructor
-  · intro h b hb
-    exact measure_mono_null (fun y hy => (lt_of_le_of_lt hy hb : _)) h
-  intro hc
-  by_cases! h : ∀ b, c ≤ b
-  · have : {a : α | f a < c} = ∅ := by
-      apply Set.eq_empty_iff_forall_notMem.2 fun x hx => ?_
-      exact (lt_irrefl _ (lt_of_lt_of_le hx (h (f x)))).elim
-    simp [this]
-  by_cases! H : ¬IsLUB (Set.Iio c) c
-  · have : c ∈ upperBounds (Set.Iio c) := fun y hy => le_of_lt hy
-    obtain ⟨b, b_up, bc⟩ : ∃ b : β, b ∈ upperBounds (Set.Iio c) ∧ b < c := by
-      simpa [IsLUB, IsLeast, this, lowerBounds] using H
-    exact measure_mono_null (fun x hx => b_up hx) (hc b bc)
-  obtain ⟨u, _, u_lt, u_lim, -⟩ :
-    ∃ u : ℕ → β,
-      StrictMono u ∧ (∀ n : ℕ, u n < c) ∧ Tendsto u atTop (𝓝 c) ∧ ∀ n : ℕ, u n ∈ Set.Iio c :=
-    H.exists_seq_strictMono_tendsto_of_notMem (lt_irrefl c) h
-  have h_Union : {x | f x < c} = ⋃ n : ℕ, {x | f x ≤ u n} := by
-    ext1 x
-    simp_rw [Set.mem_iUnion, Set.mem_setOf_eq]
-    constructor <;> intro h
-    · obtain ⟨n, hn⟩ := ((tendsto_order.1 u_lim).1 _ h).exists; exact ⟨n, hn.le⟩
-    · obtain ⟨n, hn⟩ := h; exact hn.trans_lt (u_lt _)
-  rw [h_Union, measure_iUnion_null_iff]
-  intro n
-  exact hc _ (u_lt n)
+  simp_rw [eventually_const_le_iff_forall_lt_eventually_const_lt, ae_iff, not_lt]
 
 lemma ae_le_const_iff_forall_gt_measure_zero {β} [LinearOrder β] [TopologicalSpace β]
     [OrderTopology β] [FirstCountableTopology β] {μ : Measure α} (f : α → β) (c : β) :

Mathlib/Topology/Order/IsLUB.lean

@@ -432,4 +432,28 @@ theorem DenseRange.exists_seq_strictAnti_tendsto {β : Type*} [LinearOrder β] [
     ∃ u : ℕ → β, StrictAnti u ∧ (∀ n, f (u n) ∈ Ioi x) ∧ Tendsto (f ∘ u) atTop (𝓝 x) :=
   hf.exists_seq_strictMono_tendsto (α := αᵒᵈ) (β := βᵒᵈ) hmono.dual x
 
+theorem eventually_le_const_iff_forall_gt_eventually_lt_const [FirstCountableTopology α]
+    {l : Filter γ} [CountableInterFilter l] {f : γ → α} {a : α} :
+    (∀ᶠ x in l, f x ≤ a) ↔ ∀ b, a < b → ∀ᶠ x in l, f x < b where
+  mp h c hbc := h.mono <| fun x hx ↦ lt_of_le_of_lt hx hbc
+  mpr h := by
+    rcases exists_glb_Ioi a with ⟨d, hd⟩
+    obtain rfl | H0 := glb_Ioi_eq_self_or_Ioi_eq_Ici _ hd
+    · obtain h | _ := isTop_or_exists_gt d
+      · exact .of_forall (fun _ ↦ h _)
+      obtain ⟨u, -, -, hu_tt, hu_gt⟩ := hd.exists_seq_antitone_tendsto (by simpa)
+      replace h := fun n ↦ h (u n) (by grind)
+      rw [← eventually_countable_forall] at h
+      filter_upwards [h] with x hx
+      exact ge_of_tendsto hu_tt <| .of_forall <| fun n ↦ le_of_lt <| hx n
+    · specialize h d <| by simp [← Set.mem_Ioi, H0]
+      filter_upwards [h] with x hx
+      rw [← Set.compl_Iic, ← Set.compl_Iio, compl_inj_iff] at H0
+      simpa [← Set.mem_Iic, ← Set.mem_Iio, H0] using hx
+
+theorem eventually_const_le_iff_forall_lt_eventually_const_lt [FirstCountableTopology α]
+    {l : Filter γ} [CountableInterFilter l] {f : γ → α} {a : α} :
+    (∀ᶠ x in l, a ≤ f x) ↔ ∀ b, b < a → ∀ᶠ x in l, b < f x :=
+  eventually_le_const_iff_forall_gt_eventually_lt_const (α := αᵒᵈ)
+
 end OrderTopology

Mathlib/Topology/Order/LiminfLimsup.lean

@@ -366,21 +366,8 @@ variable [CountableInterFilter f] {u : β → α}
 
 theorem eventually_le_limsup (hf : IsBoundedUnder (· ≤ ·) f u := by isBoundedDefault) :
     ∀ᶠ b in f, u b ≤ f.limsup u := by
-  obtain ha | ha := isTop_or_exists_gt (f.limsup u)
-  · exact Eventually.of_forall fun _ => ha _
-  by_cases H : IsGLB (Set.Ioi (f.limsup u)) (f.limsup u)
-  · obtain ⟨u, -, -, hua, hu⟩ := H.exists_seq_antitone_tendsto ha
-    have := fun n => eventually_lt_of_limsup_lt (hu n) hf
-    exact
-      (eventually_countable_forall.2 this).mono fun b hb =>
-        ge_of_tendsto hua <| Eventually.of_forall fun n => (hb _).le
-  · obtain ⟨x, hx, xa⟩ : ∃ x, (∀ ⦃b⦄, f.limsup u < b → x ≤ b) ∧ f.limsup u < x := by
-      simp only [IsGLB, IsGreatest, lowerBounds, upperBounds, Set.mem_Ioi, Set.mem_setOf_eq,
-        not_and, not_forall, not_le, exists_prop] at H
-      exact H fun x => le_of_lt
-    filter_upwards [eventually_lt_of_limsup_lt xa hf] with y hy
-    contrapose! hy
-    exact hx hy
+  rw [eventually_le_const_iff_forall_gt_eventually_lt_const]
+  exact fun _ hc ↦ eventually_lt_of_limsup_lt hc
 
 theorem eventually_liminf_le (hf : IsBoundedUnder (· ≥ ·) f u := by isBoundedDefault) :
     ∀ᶠ b in f, f.liminf u ≤ u b :=