Update TuranDensity.lean

Author: mitchell-horner

Mathlib/Combinatorics/SimpleGraph/Extremal/TuranDensity.lean

@@ -11,6 +11,8 @@ public import Mathlib.Combinatorics.SimpleGraph.DeleteEdges
 public import Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
 public import Mathlib.Data.Nat.Choose.Cast
 
+import Mathlib.Topology.Instances.Real.Lemmas
+
 /-!
 # Turán density
 
@@ -78,11 +80,15 @@ noncomputable def turanDensity (H : SimpleGraph W) :=
 
 theorem isGLB_turanDensity (H : SimpleGraph W) :
     IsGLB { (extremalNumber n H / n.choose 2 : ℝ) | n ∈ Set.Ici 2 } (turanDensity H) := by
-  apply Real.isGLB_limUnder_of_bddBelow_antitoneOn_Ici
-  · refine ⟨0, fun x ⟨_, _, hx⟩ ↦ ?_⟩
+  have h_bdd : BddBelow { (extremalNumber n H / n.choose 2 : ℝ) | n ∈ Set.Ici 2 } := by
+    refine ⟨0, fun x ⟨_, _, hx⟩ ↦ ?_⟩
     rw [← hx]
     positivity
-  · exact antitoneOn_extremalNumber_div_choose_two H
+  refine Real.isGLB_of_tendsto_antitoneOn_bddBelow_nat_Ici ?_
+    (antitoneOn_extremalNumber_div_choose_two H) h_bdd
+  have h_tto := Real.tendsto_atTop_csInf_of_antitoneOn_bddBelow_nat_Ici
+    (antitoneOn_extremalNumber_div_choose_two H) h_bdd
+  rwa [← h_tto.limUnder_eq] at h_tto
 
 theorem turanDensity_eq_csInf (H : SimpleGraph W) :
     turanDensity H = sInf { (extremalNumber n H / n.choose 2 : ℝ) | n ∈ Set.Ici 2 } :=
@@ -92,8 +98,8 @@ theorem turanDensity_eq_csInf (H : SimpleGraph W) :
 /-- The **Turán density** of a simple graph `H` is well-defined. -/
 theorem tendsto_turanDensity (H : SimpleGraph W) :
     Tendsto (fun n ↦ (extremalNumber n H / n.choose 2 : ℝ)) atTop (𝓝 (turanDensity H)) := by
-  have h_tendsto := Real.tendsto_csInf_of_bddBelow_antitoneOn_Ici
-    (isGLB_turanDensity H).bddBelow (antitoneOn_extremalNumber_div_choose_two H)
+  have h_tendsto := Real.tendsto_atTop_csInf_of_antitoneOn_bddBelow_nat_Ici
+    (antitoneOn_extremalNumber_div_choose_two H) (isGLB_turanDensity H).bddBelow
   rwa [turanDensity, h_tendsto.limUnder_eq]
 
 /-- `extremalNumber n H` is asymptotically equivalent to `turanDensity H * n.choose 2` as `n`

Mathlib/Topology/Instances/NNReal/Lemmas.lean

@@ -5,7 +5,6 @@ Authors: Johan Commelin
 -/
 module
 
-public import Mathlib.Algebra.Order.Monoid.Canonical.Basic
 public import Mathlib.Data.NNReal.Basic
 public import Mathlib.Topology.Algebra.InfiniteSum.Order
 public import Mathlib.Topology.Algebra.InfiniteSum.Ring
@@ -221,93 +220,17 @@ def powOrderIso (n : ℕ) (hn : n ≠ 0) : ℝ≥0 ≃o ℝ≥0 :=
 
 section Monotone
 
-/-- A monotone, bounded above sequence `f : ℕ → ℝ` has the finite limit `iSup f`. -/
-theorem _root_.Real.tendsto_ciSup_of_bddAbove_monotone {f : ℕ → ℝ}
-    (h_bdd : BddAbove (range f)) (h_mon : Monotone f) :
-    Tendsto f atTop (𝓝 (iSup f)) := by
-  obtain ⟨B, h_lub⟩ := Real.exists_isLUB (range_nonempty f) h_bdd
-  have h_sup : iSup f = B := h_lub.csSup_eq (range_nonempty f)
-  rw [h_sup]
-  exact tendsto_atTop_isLUB h_mon h_lub
-
-/-- An antitone, bounded below sequence `f : ℕ → ℝ` has the finite limit `iInf f`. -/
-theorem _root_.Real.tendsto_ciInf_of_bddBelow_antitone {f : ℕ → ℝ}
-    (h_bdd : BddBelow (range f)) (h_ant : Antitone f) :
-    Tendsto f atTop (𝓝 (iInf f)) := by
-  obtain ⟨B, h_glb⟩ := Real.exists_isGLB (range_nonempty f) h_bdd
-  have h_inf : iInf f = B := h_glb.csInf_eq (range_nonempty f)
-  rw [h_inf]
-  exact tendsto_atTop_isGLB h_ant h_glb
-
-/-- A monotone, bounded above sequence `f : ℕ → ℝ` on `Ici k` has the finite
-limit `sSup (f '' Ici k)`. -/
-theorem _root_.Real.tendsto_csSup_of_bddAbove_monotoneOn_Ici {f : ℕ → ℝ} {k : ℕ}
-    (h_bdd : BddAbove (f '' Ici k)) (h_mon : MonotoneOn f (Ici k)) :
-    Tendsto f atTop (𝓝 (sSup (f '' Ici k))) := by
-  rw [← range_add_eq_image_Ici] at h_bdd
-  rw [Ici, ← monotone_add_nat_iff_monotoneOn_nat_Ici] at h_mon
-  have h := Real.tendsto_ciSup_of_bddAbove_monotone h_bdd h_mon
-  rwa [tendsto_add_atTop_iff_nat k, ← sSup_range,
-    range_add_eq_image_Ici, image] at h
-
-/-- An antitone, bounded below sequence `f : ℕ → ℝ` on `Ici k` has the finite
-limit `sInf (f '' Ici k)`. -/
-theorem _root_.Real.tendsto_csInf_of_bddBelow_antitoneOn_Ici {f : ℕ → ℝ} {k : ℕ}
-    (h_bdd : BddBelow (f '' Ici k)) (h_ant : AntitoneOn f (Ici k)) :
-    Tendsto f atTop (𝓝 (sInf (f '' Ici k))) := by
-  rw [← range_add_eq_image_Ici] at h_bdd
-  rw [Ici, ← antitone_add_nat_iff_antitoneOn_nat_Ici] at h_ant
-  have h := Real.tendsto_ciInf_of_bddBelow_antitone h_bdd h_ant
-  rwa [tendsto_add_atTop_iff_nat k, ← sInf_range,
-    range_add_eq_image_Ici, image] at h
-
-/-- The limit of a monotone, bounded above sequence `f : ℕ → ℝ` is a least upper bound
-of the sequence. -/
-theorem _root_.Real.isLUB_limUnder_of_bddAbove_monotone {f : ℕ → ℝ}
-    (h_bdd : BddAbove (range f)) (h_mon : Monotone f) :
-    IsLUB (range f) (limUnder atTop f) := by
-  have h := Real.tendsto_ciSup_of_bddAbove_monotone h_bdd h_mon
-  rw [h.limUnder_eq]
-  exact isLUB_ciSup h_bdd
-
-/-- The limit of an antitone, bounded below sequence `f : ℕ → ℝ` is a greatest lower bound
-of the sequence. -/
-theorem _root_.Real.isGLB_limUnder_of_bddBelow_antitone {f : ℕ → ℝ}
-    (h_bdd : BddBelow (range f)) (h_ant : Antitone f) :
-    IsGLB (range f) (limUnder atTop f) := by
-  have h := Real.tendsto_ciInf_of_bddBelow_antitone h_bdd h_ant
-  rw [h.limUnder_eq]
-  exact isGLB_ciInf h_bdd
-
-/-- The limit of an antitone, bounded below sequence `f : ℕ → ℝ` on `Ici k` is a least
-upper bound of the sequence. -/
-theorem _root_.Real.isLUB_limUnder_of_bddAbove_monotoneOn_Ici {f : ℕ → ℝ} {k : ℕ}
-    (h_bdd : BddAbove (f '' Ici k)) (h_mon : MonotoneOn f (Ici k)) :
-    IsLUB (f '' Ici k) (limUnder atTop f) := by
-  have h := Real.tendsto_csSup_of_bddAbove_monotoneOn_Ici h_bdd h_mon
-  rw [h.limUnder_eq]
-  exact isLUB_csSup (image_nonempty.mpr nonempty_Ici) h_bdd
-
-/-- The limit of an antitone, bounded below sequence `f : ℕ → ℝ` on `Ici k` is a greatest
-lower bound of the sequence. -/
-theorem _root_.Real.isGLB_limUnder_of_bddBelow_antitoneOn_Ici {f : ℕ → ℝ} {k : ℕ}
-    (h_bdd : BddBelow (f '' Ici k)) (h_ant : AntitoneOn f (Ici k)) :
-    IsGLB (f '' Ici k) (limUnder atTop f) := by
-  have h := Real.tendsto_csInf_of_bddBelow_antitoneOn_Ici h_bdd h_ant
-  rw [h.limUnder_eq]
-  exact isGLB_csInf (image_nonempty.mpr nonempty_Ici) h_bdd
-
--- TODO remove `Real.tendsto_of_bddAbove_monotone` entirely
 /-- A monotone, bounded above sequence `f : ℕ → ℝ` has a finite limit. -/
-theorem _root_.Real.tendsto_of_bddAbove_monotone {f : ℕ → ℝ} (h_bdd : BddAbove (range f))
-    (h_mon : Monotone f) : ∃ r : ℝ, Tendsto f atTop (𝓝 r) :=
-  ⟨iSup f, Real.tendsto_ciSup_of_bddAbove_monotone h_bdd h_mon⟩
+theorem _root_.Real.tendsto_of_bddAbove_monotone {f : ℕ → ℝ} (h_bdd : BddAbove (Set.range f))
+    (h_mon : Monotone f) : ∃ r : ℝ, Tendsto f atTop (𝓝 r) := by
+  obtain ⟨B, hB⟩ := Real.exists_isLUB (Set.range_nonempty f) h_bdd
+  exact ⟨B, tendsto_atTop_isLUB h_mon hB⟩
 
--- TODO remove `Real.tendsto_of_bddBelow_antitone` entirely
 /-- An antitone, bounded below sequence `f : ℕ → ℝ` has a finite limit. -/
-theorem _root_.Real.tendsto_of_bddBelow_antitone {f : ℕ → ℝ} (h_bdd : BddBelow (range f))
-    (h_ant : Antitone f) : ∃ r : ℝ, Tendsto f atTop (𝓝 r) :=
-  ⟨iInf f, Real.tendsto_ciInf_of_bddBelow_antitone h_bdd h_ant⟩
+theorem _root_.Real.tendsto_of_bddBelow_antitone {f : ℕ → ℝ} (h_bdd : BddBelow (Set.range f))
+    (h_ant : Antitone f) : ∃ r : ℝ, Tendsto f atTop (𝓝 r) := by
+  obtain ⟨B, hB⟩ := Real.exists_isGLB (Set.range_nonempty f) h_bdd
+  exact ⟨B, tendsto_atTop_isGLB h_ant hB⟩
 
 /-- An antitone sequence `f : ℕ → ℝ≥0` has a finite limit. -/
 theorem tendsto_of_antitone {f : ℕ → ℝ≥0} (h_ant : Antitone f) :