Created
July 18, 2025 21:44
-
-
Save cmrfrd/e2acc96fd0a53ef11e6a70411af3f78d to your computer and use it in GitHub Desktop.
lean proof of density of the rationals
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| import Mathlib.Tactic | |
| import Mathlib.Algebra.Field.Basic | |
| import Mathlib.Topology.Basic | |
| import Mathlib.Topology.Order.Basic | |
| import Mathlib.Data.Real.Basic | |
| import Mathlib.Data.Real.Basic | |
| import Mathlib.Data.Rat.Defs | |
| import Mathlib.Data.Int.Cast.Lemmas | |
| import Mathlib.Topology.MetricSpace.Basic | |
| import Mathlib.Topology.Constructions | |
| import Mathlib.Algebra.Order.Field.Basic | |
| open Real Set | |
| -- Density in this statement implies we can always find some | |
| -- rational `q` arbitrarily close to x. | |
| lemma h_dense (x : ℝ) : ∀ ε > 0, ∃ q : ℚ, |x - q| < ε := by { | |
| intro e he | |
| -- We first define `n` and `m` which will approximate `q` as `m / n` | |
| -- where `e` is our "error". This means that as `e -> 0`, then | |
| -- `m / n ≈ x` | |
| let n : ℕ := ⌈1 / e⌉.toNat + 1 | |
| let m : ℤ := Int.floor (x * n) | |
| use m / n | |
| simp | |
| -- Our goal now is to show `|x - ↑m / ↑n| < e` | |
| -- first we will rewrite it without division | |
| have hn : 0 < (n : ℝ) := Nat.cast_pos.mpr (Nat.succ_pos _) | |
| have : |x - m / n| = |x * n - m| / n := by { | |
| field_simp [hn.ne'] | |
| rw [div_eq_mul_inv, abs_mul, abs_of_pos (inv_pos.mpr hn)] | |
| field_simp | |
| } | |
| rw [this] | |
| refine (div_lt_iff₀ hn).mpr ?_ | |
| -- Now we will prove this `|x * ↑n - ↑m| < e * ↑n` | |
| -- via triangle inequality or | |
| -- `|x * ↑n - ↑m| < 1 < e * ↑n` | |
| have abs_lt_one : |x * ↑n - ↑m| < 1 := by { | |
| have lower := Int.floor_le (x * n) | |
| have upper := Int.lt_floor_add_one (x * n) | |
| rw [abs_of_nonneg (sub_nonneg_of_le lower)] | |
| linarith | |
| } | |
| have one_lt_en : 1 < e * ↑n := by { | |
| have n_gt_one_e_ceil : (↑n : ℝ) > ⌈1 / e⌉ := by { | |
| norm_cast | |
| unfold n | |
| field_simp | |
| } | |
| have one_div_e_lt_n : 1 / e < ↑n := (Int.le_ceil (1 / e)).trans_lt n_gt_one_e_ceil | |
| exact (div_lt_iff₀' he).mp one_div_e_lt_n | |
| } | |
| apply lt_trans abs_lt_one one_lt_en | |
| } |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment