From 57e5befe503cc52b398b7ddac9efe9f6c94d7a6f Mon Sep 17 00:00:00 2001 From: Moritz Firsching Date: Sat, 4 May 2024 21:59:55 +0200 Subject: [PATCH] Ch. 1: prove monotone_primeCountingReal (#55) --- .../Ch01_Six_proofs_of_the_infinity_of_primes.lean | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) diff --git a/FormalBook/Ch01_Six_proofs_of_the_infinity_of_primes.lean b/FormalBook/Ch01_Six_proofs_of_the_infinity_of_primes.lean index d11f69d..a47e367 100644 --- a/FormalBook/Ch01_Six_proofs_of_the_infinity_of_primes.lean +++ b/FormalBook/Ch01_Six_proofs_of_the_infinity_of_primes.lean @@ -208,7 +208,7 @@ using elementary calculus open Filter noncomputable def primeCountingReal (x : ℝ) : ℕ := - if (x > 0) then primeCounting ⌊x⌋.natAbs else 0 + if (x ≤ 0) then 0 else primeCounting ⌊x⌋₊ def S₁ (x : ℝ) : Set ℕ := { n | ∀ p, Nat.Prime p → p ∣ n → p ≤ x } @@ -229,7 +229,17 @@ theorem infinity_of_primes₄ : Tendsto π atTop atTop := by sorry -- This might be useful for the proof. Rename as you like. -theorem monotone_primeCountingReal : Monotone primeCountingReal := by sorry +theorem monotone_primeCountingReal : Monotone primeCountingReal := by + intro a b hab + unfold primeCountingReal + by_cases ha : a ≤ 0 + · by_cases hb : b ≤ 0 + · simp [ha, hb] + · simp [ha, hb] + · by_cases hb : b ≤ 0 + · linarith + · simp [ha, hb] + exact monotone_primeCounting <| Nat.floor_mono hab lemma H_P4_1 {k p: ℝ} (hk: k > 0) (hp: p ≥ k + 1): p / (p - 1) ≤ (k + 1) / k := by have h_k_nonzero: k ≠ 0 := ne_iff_lt_or_gt.mpr (Or.inr hk)