Disprove that quotients of bounded functions stay bounded

Analysis/Section_9_6.lean

@@ -187,7 +187,36 @@ theorem BddOn.mul (f g : ℝ → ℝ) (X : Set ℝ) (hf : BddOn f X) (hg : BddOn
 
 def BddOn.div : Decidable (∀ (f g : ℝ → ℝ) (X : Set ℝ) (_ : ∀ x ∈ X, g x ≠ 0) (_ : BddOn f X)
     (_: BddOn g X), (BddOn (f / g) X)) := by
-  -- the first line of this construction should be either `apply isTrue` or `apply isFalse`, depending on whether you believe the given statement to be true or false.
-  sorry
+  -- Bounded numerator and denominator need not give a bounded quotient (e.g. 1/x on (0,1)).
+  apply isFalse
+  intro h
+  let f : ℝ → ℝ := fun _ ↦ 1
+  let g : ℝ → ℝ := fun x ↦ x
+  let X : Set ℝ := Set.Ioo 0 1
+  have hg : ∀ x ∈ X, g x ≠ 0 := by
+    intro x hx; exact ne_of_gt hx.1
+  have hf : BddOn f X := ⟨1, by intro x _hx; simp [f]⟩
+  have hgB : BddOn g X := ⟨1, by
+    intro x hx
+    simp [g, abs_of_pos hx.1]
+    exact le_of_lt hx.2⟩
+  obtain ⟨M, hM⟩ := h f g X hg hf hgB
+  have hhalf : (1 / 2 : ℝ) ∈ X := by constructor <;> norm_num
+  have hMnonneg : 0 ≤ M := (abs_nonneg _).trans (hM (1 / 2) hhalf)
+  -- Always in (0, 1/2] ⊆ (0,1) when M ≥ 0.
+  let x : ℝ := 1 / (M + 2)
+  have hxX : x ∈ X := by
+    refine ⟨by positivity, ?_⟩
+    have : (1 : ℝ) / (M + 2) ≤ 1 / 2 := by
+      apply one_div_le_one_div_of_le <;> linarith
+    linarith
+  have hxpos : 0 < x := by positivity
+  have hval : |(f / g) x| = (M + 2 : ℝ) := by
+    simp [f, g, Pi.div_apply, x, abs_of_pos (one_div_pos.mpr hxpos),
+      abs_of_nonneg (show (0:ℝ) ≤ M + 2 by linarith), one_div_div]
+  have : (M + 2 : ℝ) ≤ M := by
+    have := hM x hxX
+    rwa [hval] at this
+  linarith
 
 end Chapter9