From e83387c60c112c70a8b096f0078a3b41248b80e9 Mon Sep 17 00:00:00 2001 From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Tue, 24 Sep 2024 00:45:25 +0200 Subject: [PATCH 01/13] wip --- PrimeNumberTheoremAnd/Consequences.lean | 298 ++++++++++++++++++++++++ 1 file changed, 298 insertions(+) diff --git a/PrimeNumberTheoremAnd/Consequences.lean b/PrimeNumberTheoremAnd/Consequences.lean index 5131aa6b..74acde6c 100644 --- a/PrimeNumberTheoremAnd/Consequences.lean +++ b/PrimeNumberTheoremAnd/Consequences.lean @@ -11,6 +11,252 @@ open Nat hiding log open Finset open BigOperators Filter Real Classical Asymptotics MeasureTheory +lemma abel_summation {a : ArithmeticFunction ℝ} (x y : ℝ) (ϕ : ℝ → ℝ) (hxy : x < y): + ∑ n ∈ Ioc ⌊x⌋₊ ⌊y⌋₊, (a n : ℝ) * ϕ n = + (∑ n ∈ Iic ⌊y⌋₊, a n) * ϕ y - (∑ n ∈ Iic ⌊x⌋₊, a n) * ϕ x - + ∫ u in Set.Icc x y, (∑ n ∈ Iic ⌊u⌋₊, a n) * (deriv ϕ) u := by + let m := ⌊x⌋₊ + let k := ⌊y⌋₊ + let A (z : ℝ) := ∑ j ∈ Iic ⌊z⌋₊, a j + calc + _ = ∑ n ∈ Ioc m k, (A n - A (n - 1)) * ϕ n := ?_ + _ = ∑ n ∈ Ioc m k, A n * ϕ n - ∑ n ∈ Ico m k, A n * ϕ (n + 1) := ?_ + _ = ∑ n ∈ Ioo m k, A n * (ϕ n - ϕ (n + 1)) + A k * ϕ k - A m * ϕ (m + 1) := ?_ + _ = - ∑ n ∈ Ioo m k, A n * (∫ t in Set.Icc (n : ℝ) (n + 1), deriv ϕ t) + A k * ϕ k - A m * ϕ (m + 1) := ?_ + _ = - ∑ n ∈ Ioo m k, (∫ t in Set.Icc (n : ℝ) (n + 1), A t * deriv ϕ t) + A k * ϕ k - A m * ϕ (m + 1) := ?_ + _ = - (∫ t in Set.Icc (m + 1 : ℝ) k, A t * deriv ϕ t) + A k * ϕ k - A m * ϕ (m + 1) := ?_ + _ = - (∫ t in Set.Icc (m + 1 : ℝ) k, A t * deriv ϕ t) + + A y * ϕ y + - (∫ t in Set.Icc (k : ℝ) y, A t * deriv ϕ t) + - A x * ϕ x + - (∫ t in Set.Icc (x : ℝ) (m + 1), A t * deriv ϕ t) := ?_ + _ = A y * ϕ y - A x * ϕ x - (∫ t in Set.Icc x y, A t * deriv ϕ t) := ?_ + · have h1 (n : ℕ) (hn : n ≠ 0) : A n - A (n - 1) = a n := by + obtain ⟨n, rfl⟩ := exists_eq_succ_of_ne_zero hn + simp [A] + rw [floor_add_one] + simp only [floor_natCast] + rw [Iic_eq_Icc] + simp [← Icc_insert_succ_right] + simp + refine Finset.sum_congr rfl fun n hn => ?_ + simp only [mem_Ioc] at hn + rw [h1 _ (not_eq_zero_of_lt hn.1)] + · simp_rw [sub_mul, sum_sub_distrib] + congr 1 + apply sum_bij (fun n hn => n - 1) + · intro n hn + simp only [mem_Ioc] at hn + obtain ⟨n, rfl⟩ := exists_eq_succ_of_ne_zero (not_eq_zero_of_lt hn.1) + simp_all [Nat.lt_add_one_iff, add_one_le_iff] + · intro n₁ hn₁ n₂ hn₂ h + simp_all + apply pred_inj (pos_of_gt hn₁.1) (pos_of_gt hn₂.1) h + · intro n hn + use n + 1 + simp_all [Nat.lt_add_one_iff, add_one_le_iff] + · intro n hn + simp only [mem_Ioc] at hn + have := pos_of_gt hn.1 + rw [← cast_add_one] + rw [Nat.sub_add_cancel this] + rw [cast_pred this] + all_goals sorry +#exit +lemma nth_prime_one_eq_three : nth Nat.Prime 1 = 3 := nth_count prime_three + +@[simp] +lemma Nat.primeCounting'_eq_zero_iff {n : ℕ} : n.primeCounting' = 0 ↔ n ≤ 2 := by + refine ⟨?_, ?_⟩ + · contrapose! + intro h + replace h : 3 ≤ n := by omega + have := monotone_primeCounting' h + have := nth_prime_one_eq_three ▸ primeCounting'_nth_eq 1 + omega + · intro hn + have := zeroth_prime_eq_two ▸ primeCounting'_nth_eq 0 + have := monotone_primeCounting' hn + omega + + +@[simp] +lemma Nat.primeCounting_eq_zero_iff {n : ℕ} : n.primeCounting = 0 ↔ n ≤ 1 := by + simp [Nat.primeCounting] + +@[simp] +lemma Nat.primeCounting_zero : Nat.primeCounting 0 = 0 := + Nat.primeCounting_eq_zero_iff.mpr zero_le_one + +@[simp] +lemma Nat.primeCounting_one : Nat.primeCounting 1 = 0 := + Nat.primeCounting_eq_zero_iff.mpr le_rfl + + +-- @[simps] +-- def ArithmeticFunction.primeCounting : ArithmeticFunction ℝ where +-- toFun x := Nat.primeCounting ⌊x⌋₊ +-- map_zero' := by simp [Nat.primeCounting_zero] + +-- AkraBazzi.lean +lemma deriv_smoothingFn' {x : ℝ} (hx_pos : 0 < x) (hx : x ≠ 1) : deriv (fun x => (log x)⁻¹) x = -x⁻¹ / (log x ^ 2) := by + have : log x ≠ 0 := Real.log_ne_zero_of_pos_of_ne_one hx_pos hx + rw [deriv_inv''] <;> aesop + +lemma deriv_smoothingFn {x : ℝ} (hx : 1 < x) : deriv (fun x => (log x)⁻¹) x = -x⁻¹ / (log x ^ 2) := + deriv_smoothingFn' (by positivity) (ne_of_gt hx) + +noncomputable def th (x : ℝ) := ∑ p ∈ (Iic ⌊x⌋₊).filter Nat.Prime, Real.log p + +lemma th_def' (x : ℝ) : + th x = ∑ n ∈ Iic ⌊x⌋₊, Set.indicator (setOf Nat.Prime) (fun n => log n) n := by + unfold th + rw [sum_filter] + refine sum_congr rfl fun n _ => ?_ + simp [Set.indicator_apply] + +lemma th_eq_zero_of_lt_two {x : ℝ} (hx : x < 2) : th x = 0 := by + unfold th + convert sum_empty + ext y + simp only [mem_filter, mem_Iic, not_mem_empty, iff_false, not_and] + intro hy + have : y < 2 := by + cases lt_or_le x 0 with + | inl hx' => + have := Nat.floor_of_nonpos hx'.le + rw [this, nonpos_iff_eq_zero] at hy + rw [hy] + norm_num + | inr hx' => + rw [← Nat.cast_lt_ofNat (α := ℝ)] + apply lt_of_le_of_lt ?_ hx + refine (le_floor_iff hx').mp hy + contrapose! this + exact this.two_le + +lemma th43_b (x : ℝ) (hx : 2 ≤ x) : + Nat.primeCounting ⌊x⌋₊ = + th x / log x + ∫ t in Set.Icc 2 x, th t / (t * (Real.log t) ^ 2) := by + trans th x / log x + ∫ t in Set.Icc (3 / 2) x, th t / (t * (Real.log t) ^ 2) + swap + · congr 1 + have : Set.Icc (3/2) x = Set.Ico (3/2) 2 ∪ Set.Icc 2 x := by + symm + apply Set.Ico_union_Icc_eq_Icc ?_ hx + norm_num + rw [this, integral_union] + · simp only [add_left_eq_self] + apply integral_eq_zero_of_ae + simp only [measurableSet_Ico, ae_restrict_eq] + refine eventuallyEq_inf_principal_iff.mpr ?_ + apply Eventually.of_forall + intro y hy + simp only [Set.mem_Ico] at hy + have := th_eq_zero_of_lt_two hy.2 + simp_all + · rw [Set.disjoint_iff, Set.subset_empty_iff] + ext y + simp (config := {contextual := true}) + · exact measurableSet_Icc + · rw [integrableOn_congr_fun (g := 0)] + exact integrableOn_zero + · intro y hy + simp only [Set.mem_Ico] at hy + have := th_eq_zero_of_lt_two hy.2 + simp_all + · exact measurableSet_Ico + · unfold th + -- fun_prop + sorry + + have h1 (r : ℝ) : ∑ p ∈ (Iic ⌊r⌋₊).filter Nat.Prime, Real.log p = + ∑ p ∈ (Iic ⌊r⌋₊), if p.Prime then Real.log p else 0 := by + rw [sum_filter] + -- simp_rw [h1] + let a : ArithmeticFunction ℝ := { + toFun := Set.indicator (setOf Nat.Prime) (fun n => log n) + map_zero' := by simp + } + have h3 (n : ℕ) : a n * (log n)⁻¹ = if n.Prime then 1 else 0 := by + simp only [coe_mk, ite_mul, zero_mul, a] + simp [Set.indicator_apply] + split_ifs with h + · refine mul_inv_cancel₀ ?_ + refine log_ne_zero_of_pos_of_ne_one ?_ ?_ <;> norm_cast + exacts [h.pos, h.ne_one] + · rfl + -- stop + have h2 := abel_summation (ϕ := fun x => (log x)⁻¹) (a := a) (3 / 2) x + have h4 : ⌊(3/2 : ℝ)⌋₊ = 1 := by rw [@floor_div_ofNat]; rw [Nat.floor_ofNat] + have h5 : Iic 1 = {0, 1} := by ext; simp; omega + have h6 (N : ℕ) : (filter Nat.Prime (Ioc 1 N)).card = Nat.primeCounting N := by + have : filter Nat.Prime (Ioc 1 N) = filter Nat.Prime (range (N + 1)) := by + ext n + simp only [mem_filter, mem_Ioc, mem_range, and_congr_left_iff] + intro hn + simp [lt_succ, hn.one_lt] + rw [this] + simp [primeCounting, primeCounting', count_eq_card_filter_range] + have h7 : a 1 = 0 := by + simp [a] + have h8 (f : ℝ → ℝ) : + ∫ (u : ℝ) in Set.Icc (3 / 2) x, f u * deriv (fun x ↦ (log x)⁻¹) u = + ∫ (u : ℝ) in Set.Icc (3 / 2) x, f u * -(u * log u ^ 2)⁻¹ := by + apply setIntegral_congr_ae + · exact measurableSet_Icc + refine Eventually.of_forall (fun u hu => ?_) + have hu' : 1 < u := by + simp at hu + calc + (1 : ℝ) < 3/2 := by norm_num + _ ≤ u := hu.1 + rw [deriv_smoothingFn hu'] + congr + simp [div_eq_mul_inv, mul_comm] + simp [h3, h4, h5, h6, h7, h8, integral_neg] at h2 + rw [h2] + simp [a, ← th_def', div_eq_mul_inv] + + +-- lemma th43_b' (x : ℝ) (hx : 2 ≤ x) : +-- Nat.primeCounting ⌊x⌋₊ = +-- (Real.log x)⁻¹ * ∑ p ∈ (Iic ⌊x⌋₊).filter Nat.Prime, Real.log p + +-- ∫ t in Set.Icc 2 x, +-- (∑ p ∈ (Iic ⌊t⌋₊).filter Nat.Prime, Real.log p) * (t * (Real.log t) ^ 2)⁻¹ := by +-- have h1 (r : ℝ) : ∑ p ∈ (Iic ⌊r⌋₊).filter Nat.Prime, Real.log p = +-- ∑ p ∈ (Iic ⌊r⌋₊), if p.Prime then Real.log p else 0 := by +-- rw [sum_filter] +-- -- simp_rw [h1] +-- have h2 := abel_summation (ϕ := fun x => (log x)⁻¹) (a := ArithmeticFunction.primeCounting) (3 / 2) x +-- simp [ArithmeticFunction.primeCounting] at h2 +-- have : ⌊(3/2 : ℝ)⌋₊ = 1 := by rw [@floor_div_ofNat]; rw [Nat.floor_ofNat] +-- simp [this] at h2 +-- have : Iic 1 = {0, 1} := by ext; simp; omega +-- simp [this] at h2 +-- rw [eq_sub_iff_add_eq, add_comm, ← eq_sub_iff_add_eq] at h2 +-- -- rw [← sub_mul] at h2 +-- -- rw [← Finset.sum_sdiff_eq_sub] at h2 +-- have := deriv_smoothingFn (one_lt_two.trans_le hx) +-- have : +-- ∫ (u : ℝ) in Set.Icc (3 / 2) x, (∑ x ∈ Iic ⌊u⌋₊, ↑x.primeCounting) * deriv (fun x ↦ (log x)⁻¹) u = +-- ∫ (u : ℝ) in Set.Icc (3 / 2) x, (∑ x ∈ Iic ⌊u⌋₊, ↑x.primeCounting) * -(u * log u ^ 2)⁻¹ := by +-- apply setIntegral_congr_ae +-- · exact measurableSet_Icc +-- refine Eventually.of_forall (fun u hu => ?_) +-- have hu' : 1 < u := by +-- simp at hu +-- calc +-- (1 : ℝ) < 3/2 := by norm_num +-- _ ≤ u := hu.1 +-- rw [deriv_smoothingFn hu'] +-- congr +-- simp [div_eq_mul_inv, mul_comm] +-- simp [this, ← sum_mul] at h2 + + +-- done +-- #exit /-%% \begin{lemma}\label{range-eq-range}\lean{finsum_range_eq_sum_range, finsum_range_eq_sum_range'}\leanok For any arithmetic function $f$ and real number $x$, one has $$ \sum_{n \leq x} f(n) = \sum_{n \leq ⌊x⌋_+} f(n)$$ @@ -404,6 +650,58 @@ as $x \to \infty$. theorem pi_asymp : ∃ c : ℝ → ℝ, c =o[atTop] (fun _ ↦ (1:ℝ)) ∧ ∀ x : ℝ, Nat.primeCounting ⌊x⌋₊ = (1 + c x) * ∫ t in Set.Icc 2 x, 1 / (log t) ∂ volume := by + have h0 (x : ℝ) : + ∫ t in Set.Icc 2 x, + (∑ p ∈ (Iic ⌊t⌋₊).filter Nat.Prime, Real.log p) * (t * (Real.log t) ^ 2)⁻¹ = 0 := by + simp_rw [sum_mul] + convert + @MeasureTheory.integral_finset_sum + ℝ + _ + _ + _ + _ + (volume.restrict (Set.Icc (2 : ℝ) x)) + ℕ + ((Iic ⌊x⌋₊).filter Nat.Prime) + (fun i t => log ↑i * (t * log t ^ 2)⁻¹) + ?_ + using 1 + with u + done + have h1 (x : ℝ) : Nat.primeCounting ⌊x⌋₊ = + (Real.log x)⁻¹ * ∑ p ∈ (Iic ⌊x⌋₊).filter Nat.Prime, Real.log p + + ∫ t in Set.Icc 2 x, + (∑ p ∈ (Iic ⌊t⌋₊).filter Nat.Prime, Real.log p) * (t * (Real.log t) ^ 2)⁻¹ := by + -- can be proven by interchanging the sum and integral and using the fundamental theorem of + -- calculus + simp_rw [sum_mul] + rw [@MeasureTheory.integral_finset_sum + ℝ + _ + _ + _ + _ + (volume.restrict (Set.Icc (2 : ℝ) x)) + ℕ + ((Iic ⌊x⌋₊).filter Nat.Prime) + fun i t => log ↑i * (t * log t ^ 2)⁻¹ + ] + + rw [← MeasureTheory.integral_subtype] + + rw [@MeasureTheory.integral_finset_sum + (Set.Icc 2 x) + _ + _ + _ + _ + volume + (ι := ℕ) (s := (Iic ⌊x⌋₊).filter Nat.Prime) + ] + sorry + #check chebyshev_asymptotic + -- have h2 (ε : ℝ) : ∃ xε := chebyshev_asymptotic sorry /-%% From 95c2ebcc8d53bb35497ed94dcb7050f321f1f8ec Mon Sep 17 00:00:00 2001 From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Tue, 24 Sep 2024 01:13:01 +0200 Subject: [PATCH 02/13] wip --- PrimeNumberTheoremAnd/Consequences.lean | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/PrimeNumberTheoremAnd/Consequences.lean b/PrimeNumberTheoremAnd/Consequences.lean index 74acde6c..8cd64a60 100644 --- a/PrimeNumberTheoremAnd/Consequences.lean +++ b/PrimeNumberTheoremAnd/Consequences.lean @@ -61,6 +61,19 @@ lemma abel_summation {a : ArithmeticFunction ℝ} (x y : ℝ) (ϕ : ℝ → ℝ) rw [← cast_add_one] rw [Nat.sub_add_cancel this] rw [cast_pred this] + · have : m ≤ k := by simp [m, k, Nat.floor_le_floor hxy.le] + cases this.eq_or_lt with + | inl hmk => + rw [hmk] + simp + sorry + | inr hmk => + rw [← Ioo_insert_right hmk, ← Ioo_insert_left hmk] + rw [sum_insert left_not_mem_Ioo, sum_insert right_not_mem_Ioo] + simp_rw [mul_sub, sum_sub_distrib] + abel + · -- FTC-2 + sorry all_goals sorry #exit lemma nth_prime_one_eq_three : nth Nat.Prime 1 = 3 := nth_count prime_three From 2bc2e5b6aef08e6c13b7ffcea916173101ab08f1 Mon Sep 17 00:00:00 2001 From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Wed, 25 Sep 2024 23:18:45 +0200 Subject: [PATCH 03/13] wip --- PrimeNumberTheoremAnd/Consequences.lean | 110 +++++++++++++++++++----- 1 file changed, 89 insertions(+), 21 deletions(-) diff --git a/PrimeNumberTheoremAnd/Consequences.lean b/PrimeNumberTheoremAnd/Consequences.lean index 8cd64a60..93dc76ea 100644 --- a/PrimeNumberTheoremAnd/Consequences.lean +++ b/PrimeNumberTheoremAnd/Consequences.lean @@ -10,27 +10,54 @@ open ArithmeticFunction hiding log open Nat hiding log open Finset open BigOperators Filter Real Classical Asymptotics MeasureTheory - -lemma abel_summation {a : ArithmeticFunction ℝ} (x y : ℝ) (ϕ : ℝ → ℝ) (hxy : x < y): +#check intervalIntegral.integral_deriv_eq_sub' +lemma abel_summation {a : ArithmeticFunction ℝ} (x y : ℝ) (hx : 0 < x) (hxy : x < y) + (ϕ : ℝ → ℝ) (hϕ : ContDiff ℝ 1 ϕ) : ∑ n ∈ Ioc ⌊x⌋₊ ⌊y⌋₊, (a n : ℝ) * ϕ n = (∑ n ∈ Iic ⌊y⌋₊, a n) * ϕ y - (∑ n ∈ Iic ⌊x⌋₊, a n) * ϕ x - ∫ u in Set.Icc x y, (∑ n ∈ Iic ⌊u⌋₊, a n) * (deriv ϕ) u := by let m := ⌊x⌋₊ let k := ⌊y⌋₊ + have : m ≤ k := by simp [m, k, Nat.floor_le_floor hxy.le] + cases this.eq_or_lt with + | inl hmk => + simp [m, k] at hmk + rw [hmk] + rw [Ioc_self] + simp + rw [← mul_sub, eq_comm, sub_eq_zero] + rw [← intervalIntegral.integral_deriv_eq_sub, ← intervalIntegral.integral_const_mul] + rw [intervalIntegral.integral_of_le hxy.le] + rw [integral_Ioc_eq_integral_Ioo] + rw [integral_Icc_eq_integral_Ioo] + apply setIntegral_congr + · exact measurableSet_Ioo + · intro z hz + have : ⌊z⌋₊ = ⌊y⌋₊ := by + simp only [Set.mem_Ioo] at hz + apply le_antisymm + · exact Nat.floor_le_floor hz.2.le + · rw [← hmk] + exact Nat.floor_le_floor hz.1.le + simp [this] + · intros + exact hϕ.differentiable le_rfl |>.differentiableAt + · exact hϕ.continuous_deriv le_rfl |>.continuousOn |>.intervalIntegrable + | inr hmk => let A (z : ℝ) := ∑ j ∈ Iic ⌊z⌋₊, a j calc _ = ∑ n ∈ Ioc m k, (A n - A (n - 1)) * ϕ n := ?_ _ = ∑ n ∈ Ioc m k, A n * ϕ n - ∑ n ∈ Ico m k, A n * ϕ (n + 1) := ?_ _ = ∑ n ∈ Ioo m k, A n * (ϕ n - ϕ (n + 1)) + A k * ϕ k - A m * ϕ (m + 1) := ?_ - _ = - ∑ n ∈ Ioo m k, A n * (∫ t in Set.Icc (n : ℝ) (n + 1), deriv ϕ t) + A k * ϕ k - A m * ϕ (m + 1) := ?_ - _ = - ∑ n ∈ Ioo m k, (∫ t in Set.Icc (n : ℝ) (n + 1), A t * deriv ϕ t) + A k * ϕ k - A m * ϕ (m + 1) := ?_ - _ = - (∫ t in Set.Icc (m + 1 : ℝ) k, A t * deriv ϕ t) + A k * ϕ k - A m * ϕ (m + 1) := ?_ - _ = - (∫ t in Set.Icc (m + 1 : ℝ) k, A t * deriv ϕ t) + _ = - ∑ n ∈ Ioo m k, A n * (∫ t in (n : ℝ)..(n + 1), deriv ϕ t) + A k * ϕ k - A m * ϕ (m + 1) := ?_ + _ = - ∑ n ∈ Ioo m k, (∫ t in (n : ℝ)..(n + 1), A t * deriv ϕ t) + A k * ϕ k - A m * ϕ (m + 1) := ?_ + _ = - (∫ t in (m + 1 : ℝ)..k, A t * deriv ϕ t) + A k * ϕ k - A m * ϕ (m + 1) := ?_ + _ = - (∫ t in (m + 1 : ℝ)..k, A t * deriv ϕ t) + A y * ϕ y - - (∫ t in Set.Icc (k : ℝ) y, A t * deriv ϕ t) + - (∫ t in (k : ℝ)..y, A t * deriv ϕ t) - A x * ϕ x - - (∫ t in Set.Icc (x : ℝ) (m + 1), A t * deriv ϕ t) := ?_ - _ = A y * ϕ y - A x * ϕ x - (∫ t in Set.Icc x y, A t * deriv ϕ t) := ?_ + - (∫ t in (x : ℝ)..(m + 1), A t * deriv ϕ t) := ?_ + _ = A y * ϕ y - A x * ϕ x - (∫ t in x..y, A t * deriv ϕ t) := ?_ · have h1 (n : ℕ) (hn : n ≠ 0) : A n - A (n - 1) = a n := by obtain ⟨n, rfl⟩ := exists_eq_succ_of_ne_zero hn simp [A] @@ -61,19 +88,60 @@ lemma abel_summation {a : ArithmeticFunction ℝ} (x y : ℝ) (ϕ : ℝ → ℝ) rw [← cast_add_one] rw [Nat.sub_add_cancel this] rw [cast_pred this] - · have : m ≤ k := by simp [m, k, Nat.floor_le_floor hxy.le] - cases this.eq_or_lt with - | inl hmk => - rw [hmk] - simp - sorry - | inr hmk => - rw [← Ioo_insert_right hmk, ← Ioo_insert_left hmk] - rw [sum_insert left_not_mem_Ioo, sum_insert right_not_mem_Ioo] - simp_rw [mul_sub, sum_sub_distrib] - abel + · rw [← Ioo_insert_right hmk, ← Ioo_insert_left hmk] + rw [sum_insert left_not_mem_Ioo, sum_insert right_not_mem_Ioo] + simp_rw [mul_sub, sum_sub_distrib] + abel · -- FTC-2 - sorry + rw [← sum_neg_distrib] + congr 2 + apply sum_congr rfl fun n hn => ?_ + rw [intervalIntegral.integral_deriv_eq_sub] + · rw [neg_mul_eq_mul_neg, neg_sub] + · intros + exact hϕ.differentiable le_rfl |>.differentiableAt + · exact hϕ.continuous_deriv le_rfl |>.continuousOn |>.intervalIntegrable + · congr 3 + apply sum_congr rfl fun n hn => ?_ + rw [← intervalIntegral.integral_const_mul] + refine intervalIntegral.integral_congr_ae ?_ + apply eventually_iff.mpr + simp only [le_add_iff_nonneg_right, zero_le_one, Set.uIoc_of_le, Set.mem_Ioc, + mul_eq_mul_right_iff, and_imp] + rw [mem_ae_iff, ← nonpos_iff_eq_zero, ← volume_singleton (a := n + 1)] + apply measure_mono + intro y hy + simp_all only [mem_Ioo, Set.mem_compl_iff, Set.mem_setOf_eq, Classical.not_imp, not_or, + Set.mem_singleton_iff] + by_contra hy' + have : ⌊y⌋₊ = n := by + rw [Nat.floor_eq_iff (n.cast_nonneg.trans hy.1.le)] + exact ⟨hy.1.le, lt_of_le_of_ne hy.2.1 hy'⟩ + apply hy.2.2.1 + simp only [← this, A, floor_natCast] + · congr 2 + rw [← Ico_succ_left] + have : m.succ ≤ k := by + rwa [Nat.succ_le_iff] + simp_rw [← Nat.cast_add_one] + rw [intervalIntegral.sum_integral_adjacent_intervals_Ico this] + intro n hn + apply IntervalIntegrable.mul_continuousOn + · simp [A] + rw [intervalIntegrable_iff_integrableOn_Ioo_of_le, IntegrableOn] + apply MeasureTheory.Integrable.congr (MeasureTheory.integrable_const (∑ j ∈ Iic n, a j)) + · simp + rw [@eventuallyEq_inf_principal_iff] + apply Eventually.of_forall + intro x hx + replace hx : ⌊x⌋₊ = n := by + simp at hx + rw [Nat.floor_eq_iff (n.cast_nonneg.trans hx.1.le)] + exact ⟨hx.1.le, hx.2⟩ + simp [hx] + · rw [← Nat.cast_add_one, cast_le] + exact n.lt_add_one.le + · exact hϕ.continuous_deriv le_rfl |>.continuousOn all_goals sorry #exit lemma nth_prime_one_eq_three : nth Nat.Prime 1 = 3 := nth_count prime_three From 7bbaf10add62fef96c31da9b54e262d0a1e135dc Mon Sep 17 00:00:00 2001 From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Thu, 26 Sep 2024 11:48:13 +0200 Subject: [PATCH 04/13] wip --- PrimeNumberTheoremAnd/Consequences.lean | 47 +++++++++++++++++++++---- 1 file changed, 41 insertions(+), 6 deletions(-) diff --git a/PrimeNumberTheoremAnd/Consequences.lean b/PrimeNumberTheoremAnd/Consequences.lean index 93dc76ea..396bcd82 100644 --- a/PrimeNumberTheoremAnd/Consequences.lean +++ b/PrimeNumberTheoremAnd/Consequences.lean @@ -45,6 +45,32 @@ lemma abel_summation {a : ArithmeticFunction ℝ} (x y : ℝ) (hx : 0 < x) (hxy · exact hϕ.continuous_deriv le_rfl |>.continuousOn |>.intervalIntegrable | inr hmk => let A (z : ℝ) := ∑ j ∈ Iic ⌊z⌋₊, a j + have hA (z : ℝ) : A z = A ⌊z⌋₊ := by simp [A] + have hint (n : ℕ) (a b : ℝ) (h : Set.uIoc a b ⊆ Set.Icc n (n + 1)) : + ∫ t in a..b, A t * deriv ϕ t = A n * (ϕ b - ϕ a) := by + rw [← intervalIntegral.integral_deriv_eq_sub] + · rw [← intervalIntegral.integral_const_mul] + refine intervalIntegral.integral_congr_ae ?_ + apply eventually_iff.mpr + simp only [le_add_iff_nonneg_right, zero_le_one, Set.uIoc_of_le, Set.mem_Ioc, + mul_eq_mul_right_iff, and_imp] + rw [mem_ae_iff, ← nonpos_iff_eq_zero, ← volume_singleton (a := n + 1)] + apply measure_mono + intro y hy + simp only [mem_Ioo, Set.mem_compl_iff, Set.mem_setOf_eq, Classical.not_imp, not_or, + Set.mem_singleton_iff] at hy ⊢ + have hy0 := h hy.1 + simp only [Set.mem_Icc] at hy0 + apply hy0.2.eq_or_lt.resolve_right + intro hy' + have : ⌊y⌋₊ = n := by + rw [Nat.floor_eq_iff (n.cast_nonneg.trans hy0.1)] + exact ⟨hy0.1, hy'⟩ + apply hy.2.1 + simp only [← this, A, floor_natCast] + · intros + exact hϕ.differentiable le_rfl |>.differentiableAt + · exact hϕ.continuous_deriv le_rfl |>.continuousOn |>.intervalIntegrable calc _ = ∑ n ∈ Ioc m k, (A n - A (n - 1)) * ϕ n := ?_ _ = ∑ n ∈ Ioc m k, A n * ϕ n - ∑ n ∈ Ico m k, A n * ϕ (n + 1) := ?_ @@ -111,8 +137,8 @@ lemma abel_summation {a : ArithmeticFunction ℝ} (x y : ℝ) (hx : 0 < x) (hxy rw [mem_ae_iff, ← nonpos_iff_eq_zero, ← volume_singleton (a := n + 1)] apply measure_mono intro y hy - simp_all only [mem_Ioo, Set.mem_compl_iff, Set.mem_setOf_eq, Classical.not_imp, not_or, - Set.mem_singleton_iff] + simp only [mem_Ioo, Set.mem_compl_iff, Set.mem_setOf_eq, Classical.not_imp, not_or, + Set.mem_singleton_iff] at hy ⊢ by_contra hy' have : ⌊y⌋₊ = n := by rw [Nat.floor_eq_iff (n.cast_nonneg.trans hy.1.le)] @@ -127,21 +153,30 @@ lemma abel_summation {a : ArithmeticFunction ℝ} (x y : ℝ) (hx : 0 < x) (hxy rw [intervalIntegral.sum_integral_adjacent_intervals_Ico this] intro n hn apply IntervalIntegrable.mul_continuousOn - · simp [A] + · simp only [cast_add, cast_one, A] rw [intervalIntegrable_iff_integrableOn_Ioo_of_le, IntegrableOn] apply MeasureTheory.Integrable.congr (MeasureTheory.integrable_const (∑ j ∈ Iic n, a j)) - · simp - rw [@eventuallyEq_inf_principal_iff] + · simp only [measurableSet_Ioo, ae_restrict_eq] + rw [eventuallyEq_inf_principal_iff] apply Eventually.of_forall intro x hx replace hx : ⌊x⌋₊ = n := by - simp at hx + simp only [Set.mem_Ioo] at hx rw [Nat.floor_eq_iff (n.cast_nonneg.trans hx.1.le)] exact ⟨hx.1.le, hx.2⟩ simp [hx] · rw [← Nat.cast_add_one, cast_le] exact n.lt_add_one.le · exact hϕ.continuous_deriv le_rfl |>.continuousOn + · rw [hA x, hA y] + have hy : ∫ t in ↑k..y, A t * deriv ϕ t = A k * (ϕ y - ϕ k) := by + apply hint + intros z hz + have : k ≤ y := by simp [k, Nat.floor_le, (hx.trans hxy).le] + simp [this] at hz ⊢ + sorry + + sorry all_goals sorry #exit lemma nth_prime_one_eq_three : nth Nat.Prime 1 = 3 := nth_count prime_three From f497f248825937ff66acf04cf522c65133358b8e Mon Sep 17 00:00:00 2001 From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Thu, 26 Sep 2024 18:49:46 +0200 Subject: [PATCH 05/13] wip --- PrimeNumberTheoremAnd/Consequences.lean | 107 +++++++++++------------- 1 file changed, 47 insertions(+), 60 deletions(-) diff --git a/PrimeNumberTheoremAnd/Consequences.lean b/PrimeNumberTheoremAnd/Consequences.lean index 396bcd82..b435d5e5 100644 --- a/PrimeNumberTheoremAnd/Consequences.lean +++ b/PrimeNumberTheoremAnd/Consequences.lean @@ -21,15 +21,11 @@ lemma abel_summation {a : ArithmeticFunction ℝ} (x y : ℝ) (hx : 0 < x) (hxy have : m ≤ k := by simp [m, k, Nat.floor_le_floor hxy.le] cases this.eq_or_lt with | inl hmk => - simp [m, k] at hmk - rw [hmk] - rw [Ioc_self] - simp - rw [← mul_sub, eq_comm, sub_eq_zero] - rw [← intervalIntegral.integral_deriv_eq_sub, ← intervalIntegral.integral_const_mul] - rw [intervalIntegral.integral_of_le hxy.le] - rw [integral_Ioc_eq_integral_Ioo] - rw [integral_Icc_eq_integral_Ioo] + simp only [m, k] at hmk + rw [hmk,Ioc_self, sum_empty, ← mul_sub, eq_comm, sub_eq_zero, + ← intervalIntegral.integral_deriv_eq_sub, ← intervalIntegral.integral_const_mul, + intervalIntegral.integral_of_le hxy.le, integral_Ioc_eq_integral_Ioo, + integral_Icc_eq_integral_Ioo] apply setIntegral_congr · exact measurableSet_Ioo · intro z hz @@ -39,34 +35,34 @@ lemma abel_summation {a : ArithmeticFunction ℝ} (x y : ℝ) (hx : 0 < x) (hxy · exact Nat.floor_le_floor hz.2.le · rw [← hmk] exact Nat.floor_le_floor hz.1.le - simp [this] + simp only [this] · intros exact hϕ.differentiable le_rfl |>.differentiableAt · exact hϕ.continuous_deriv le_rfl |>.continuousOn |>.intervalIntegrable | inr hmk => let A (z : ℝ) := ∑ j ∈ Iic ⌊z⌋₊, a j - have hA (z : ℝ) : A z = A ⌊z⌋₊ := by simp [A] - have hint (n : ℕ) (a b : ℝ) (h : Set.uIoc a b ⊆ Set.Icc n (n + 1)) : - ∫ t in a..b, A t * deriv ϕ t = A n * (ϕ b - ϕ a) := by + have hA (z : ℝ) : A z = A ⌊z⌋₊ := by simp only [floor_natCast, A] + have hint' (a b : ℝ) (h : Set.uIoc a b ⊆ Set.Icc ⌊a⌋₊ (⌊a⌋₊ + 1)) : + ∫ t in a..b, A t * deriv ϕ t = A a * (ϕ b - ϕ a) := by rw [← intervalIntegral.integral_deriv_eq_sub] · rw [← intervalIntegral.integral_const_mul] refine intervalIntegral.integral_congr_ae ?_ apply eventually_iff.mpr simp only [le_add_iff_nonneg_right, zero_le_one, Set.uIoc_of_le, Set.mem_Ioc, mul_eq_mul_right_iff, and_imp] - rw [mem_ae_iff, ← nonpos_iff_eq_zero, ← volume_singleton (a := n + 1)] + rw [mem_ae_iff, ← nonpos_iff_eq_zero, ← volume_singleton (a := ⌊a⌋₊ + 1)] apply measure_mono - intro y hy + intro z hz simp only [mem_Ioo, Set.mem_compl_iff, Set.mem_setOf_eq, Classical.not_imp, not_or, - Set.mem_singleton_iff] at hy ⊢ - have hy0 := h hy.1 - simp only [Set.mem_Icc] at hy0 - apply hy0.2.eq_or_lt.resolve_right - intro hy' - have : ⌊y⌋₊ = n := by - rw [Nat.floor_eq_iff (n.cast_nonneg.trans hy0.1)] - exact ⟨hy0.1, hy'⟩ - apply hy.2.1 + Set.mem_singleton_iff] at hz ⊢ + have hz0 := h hz.1 + simp only [Set.mem_Icc] at hz0 + apply hz0.2.eq_or_lt.resolve_right + intro hz' + have : ⌊z⌋₊ = ⌊a⌋₊ := by + rw [Nat.floor_eq_iff ((Nat.cast_nonneg _).trans hz0.1)] + exact ⟨hz0.1, hz'⟩ + apply hz.2.1 simp only [← this, A, floor_natCast] · intros exact hϕ.differentiable le_rfl |>.differentiableAt @@ -75,7 +71,6 @@ lemma abel_summation {a : ArithmeticFunction ℝ} (x y : ℝ) (hx : 0 < x) (hxy _ = ∑ n ∈ Ioc m k, (A n - A (n - 1)) * ϕ n := ?_ _ = ∑ n ∈ Ioc m k, A n * ϕ n - ∑ n ∈ Ico m k, A n * ϕ (n + 1) := ?_ _ = ∑ n ∈ Ioo m k, A n * (ϕ n - ϕ (n + 1)) + A k * ϕ k - A m * ϕ (m + 1) := ?_ - _ = - ∑ n ∈ Ioo m k, A n * (∫ t in (n : ℝ)..(n + 1), deriv ϕ t) + A k * ϕ k - A m * ϕ (m + 1) := ?_ _ = - ∑ n ∈ Ioo m k, (∫ t in (n : ℝ)..(n + 1), A t * deriv ϕ t) + A k * ϕ k - A m * ϕ (m + 1) := ?_ _ = - (∫ t in (m + 1 : ℝ)..k, A t * deriv ϕ t) + A k * ϕ k - A m * ϕ (m + 1) := ?_ _ = - (∫ t in (m + 1 : ℝ)..k, A t * deriv ϕ t) @@ -86,12 +81,12 @@ lemma abel_summation {a : ArithmeticFunction ℝ} (x y : ℝ) (hx : 0 < x) (hxy _ = A y * ϕ y - A x * ϕ x - (∫ t in x..y, A t * deriv ϕ t) := ?_ · have h1 (n : ℕ) (hn : n ≠ 0) : A n - A (n - 1) = a n := by obtain ⟨n, rfl⟩ := exists_eq_succ_of_ne_zero hn - simp [A] - rw [floor_add_one] - simp only [floor_natCast] + simp only [succ_eq_add_one, cast_add, cast_one, cast_nonneg, floor_add_one, floor_natCast, + add_sub_cancel_right, A] rw [Iic_eq_Icc] - simp [← Icc_insert_succ_right] - simp + simp only [bot_eq_zero', _root_.zero_le, ← Icc_insert_succ_right, mem_Icc, + add_le_iff_nonpos_right, nonpos_iff_eq_zero, one_ne_zero, and_false, not_false_eq_true, + sum_insert, add_sub_cancel_right] refine Finset.sum_congr rfl fun n hn => ?_ simp only [mem_Ioc] at hn rw [h1 _ (not_eq_zero_of_lt hn.1)] @@ -101,13 +96,15 @@ lemma abel_summation {a : ArithmeticFunction ℝ} (x y : ℝ) (hx : 0 < x) (hxy · intro n hn simp only [mem_Ioc] at hn obtain ⟨n, rfl⟩ := exists_eq_succ_of_ne_zero (not_eq_zero_of_lt hn.1) - simp_all [Nat.lt_add_one_iff, add_one_le_iff] + simp_all only [floor_natCast, succ_eq_add_one, Nat.lt_add_one_iff, add_one_le_iff, + add_tsub_cancel_right, mem_Ico, and_self] · intro n₁ hn₁ n₂ hn₂ h - simp_all + simp_all only [floor_natCast, mem_Ioc] apply pred_inj (pos_of_gt hn₁.1) (pos_of_gt hn₂.1) h · intro n hn use n + 1 - simp_all [Nat.lt_add_one_iff, add_one_le_iff] + simp_all only [floor_natCast, mem_Ico, add_tsub_cancel_right, mem_Ioc, Nat.lt_add_one_iff, + add_one_le_iff, and_self, exists_const] · intro n hn simp only [mem_Ioc] at hn have := pos_of_gt hn.1 @@ -122,29 +119,12 @@ lemma abel_summation {a : ArithmeticFunction ℝ} (x y : ℝ) (hx : 0 < x) (hxy rw [← sum_neg_distrib] congr 2 apply sum_congr rfl fun n hn => ?_ - rw [intervalIntegral.integral_deriv_eq_sub] + rw [hint' n] · rw [neg_mul_eq_mul_neg, neg_sub] - · intros - exact hϕ.differentiable le_rfl |>.differentiableAt - · exact hϕ.continuous_deriv le_rfl |>.continuousOn |>.intervalIntegrable - · congr 3 - apply sum_congr rfl fun n hn => ?_ - rw [← intervalIntegral.integral_const_mul] - refine intervalIntegral.integral_congr_ae ?_ - apply eventually_iff.mpr - simp only [le_add_iff_nonneg_right, zero_le_one, Set.uIoc_of_le, Set.mem_Ioc, - mul_eq_mul_right_iff, and_imp] - rw [mem_ae_iff, ← nonpos_iff_eq_zero, ← volume_singleton (a := n + 1)] - apply measure_mono - intro y hy - simp only [mem_Ioo, Set.mem_compl_iff, Set.mem_setOf_eq, Classical.not_imp, not_or, - Set.mem_singleton_iff] at hy ⊢ - by_contra hy' - have : ⌊y⌋₊ = n := by - rw [Nat.floor_eq_iff (n.cast_nonneg.trans hy.1.le)] - exact ⟨hy.1.le, lt_of_le_of_ne hy.2.1 hy'⟩ - apply hy.2.2.1 - simp only [← this, A, floor_natCast] + · intro z hz + simp only [le_add_iff_nonneg_right, zero_le_one, Set.uIoc_of_le, Set.mem_Ioc, floor_natCast, + Set.mem_Icc] at hz ⊢ + exact ⟨hz.1.le, hz.2⟩ · congr 2 rw [← Ico_succ_left] have : m.succ ≤ k := by @@ -170,13 +150,20 @@ lemma abel_summation {a : ArithmeticFunction ℝ} (x y : ℝ) (hx : 0 < x) (hxy · exact hϕ.continuous_deriv le_rfl |>.continuousOn · rw [hA x, hA y] have hy : ∫ t in ↑k..y, A t * deriv ϕ t = A k * (ϕ y - ϕ k) := by - apply hint + apply hint' intros z hz have : k ≤ y := by simp [k, Nat.floor_le, (hx.trans hxy).le] - simp [this] at hz ⊢ - sorry - - sorry + simp only [this, Set.uIoc_of_le, Set.mem_Ioc, floor_natCast, Set.mem_Icc, k] at hz ⊢ + exact ⟨hz.1.le, hz.2.trans (Nat.lt_floor_add_one _).le⟩ + have hx : ∫ t in x..m + 1, A t * deriv ϕ t = A x * (ϕ (m + 1) - ϕ x) := by + apply hint' + intros z hz + have : x ≤ m + 1 := by simp only [(Nat.lt_floor_add_one x).le, m] + simp only [this, Set.uIoc_of_le, Set.mem_Ioc, Set.mem_Icc, m] at hz ⊢ + refine ⟨(floor_le hx.le).trans hz.1.le, hz.2⟩ + rw [hy, hx] + simp only [k, m, hA x] + ring all_goals sorry #exit lemma nth_prime_one_eq_three : nth Nat.Prime 1 = 3 := nth_count prime_three From afe0ca47ab12931b2974a5008d8f2e7629e80fd6 Mon Sep 17 00:00:00 2001 From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Sat, 28 Sep 2024 00:21:58 +0200 Subject: [PATCH 06/13] wip --- PrimeNumberTheoremAnd/Consequences.lean | 134 ++++++++++++++++++------ 1 file changed, 104 insertions(+), 30 deletions(-) diff --git a/PrimeNumberTheoremAnd/Consequences.lean b/PrimeNumberTheoremAnd/Consequences.lean index b435d5e5..f538a6b1 100644 --- a/PrimeNumberTheoremAnd/Consequences.lean +++ b/PrimeNumberTheoremAnd/Consequences.lean @@ -10,7 +10,7 @@ open ArithmeticFunction hiding log open Nat hiding log open Finset open BigOperators Filter Real Classical Asymptotics MeasureTheory -#check intervalIntegral.integral_deriv_eq_sub' + lemma abel_summation {a : ArithmeticFunction ℝ} (x y : ℝ) (hx : 0 < x) (hxy : x < y) (ϕ : ℝ → ℝ) (hϕ : ContDiff ℝ 1 ϕ) : ∑ n ∈ Ioc ⌊x⌋₊ ⌊y⌋₊, (a n : ℝ) * ϕ n = @@ -18,6 +18,7 @@ lemma abel_summation {a : ArithmeticFunction ℝ} (x y : ℝ) (hx : 0 < x) (hxy ∫ u in Set.Icc x y, (∑ n ∈ Iic ⌊u⌋₊, a n) * (deriv ϕ) u := by let m := ⌊x⌋₊ let k := ⌊y⌋₊ + have hky : k ≤ y := by simp [k, Nat.floor_le, (hx.trans hxy).le] have : m ≤ k := by simp [m, k, Nat.floor_le_floor hxy.le] cases this.eq_or_lt with | inl hmk => @@ -67,6 +68,40 @@ lemma abel_summation {a : ArithmeticFunction ℝ} (x y : ℝ) (hx : 0 < x) (hxy · intros exact hϕ.differentiable le_rfl |>.differentiableAt · exact hϕ.continuous_deriv le_rfl |>.continuousOn |>.intervalIntegrable + have hIntegrableOn (n : ℕ) (b c : ℝ) (hbc : b ≤ c) (h : Set.uIoc b c ⊆ Set.Icc n (n + 1)) : + IntegrableOn (fun t ↦ A t * deriv ϕ t) (Set.Ico b c) volume := by + obtain rfl | hbc := hbc.eq_or_lt + · simp + have h' : Set.Icc b c ⊆ Set.Icc n (n + 1) := by + rwa [← closure_Ioc hbc.ne, ← Set.uIoc_of_le hbc.le, isClosed_Icc.closure_subset_iff] + apply IntegrableOn.mul_continuousOn_of_subset ?_ ?_ + measurableSet_Ico CompactIccSpace.isCompact_Icc Set.Ico_subset_Icc_self + · simp only [cast_add, cast_one, A] + rw [IntegrableOn] + apply MeasureTheory.Integrable.congr (MeasureTheory.integrable_const (∑ j ∈ Iic n, a j)) + · simp only [measurableSet_Ico, ae_restrict_eq] + rw [eventuallyEq_inf_principal_iff] + apply Eventually.of_forall + intro z hz + replace hz : ⌊z⌋₊ = n := by + have := Set.Ico_subset_Icc_self.trans h' hz + simp only [Set.mem_Icc] at this + rw [Nat.floor_eq_iff (n.cast_nonneg.trans this.1)] + refine ⟨this.1, ?_⟩ + apply lt_of_le_of_ne this.2 + rintro rfl + have : n + 1 < c := by simp only [Set.mem_Ico] at hz; exact hz.2 + apply this.not_le + have := h' <| Set.right_mem_Icc.mpr hbc.le + simp only [Set.mem_Icc] at this + exact this.2 + simp [hz] + · exact hϕ.continuous_deriv le_rfl |>.continuousOn + have hIntervalIntegrable (n : ℕ) (b c : ℝ) (hbc : b ≤ c) (h : Set.uIoc b c ⊆ Set.Icc n (n + 1)) : + IntervalIntegrable (fun t ↦ A t * deriv ϕ t) volume b c := by + rw [intervalIntegrable_iff_integrableOn_Ico_of_le hbc] + apply hIntegrableOn n b c hbc h + calc _ = ∑ n ∈ Ioc m k, (A n - A (n - 1)) * ϕ n := ?_ _ = ∑ n ∈ Ioc m k, A n * ϕ n - ∑ n ∈ Ico m k, A n * ϕ (n + 1) := ?_ @@ -78,6 +113,10 @@ lemma abel_summation {a : ArithmeticFunction ℝ} (x y : ℝ) (hx : 0 < x) (hxy - (∫ t in (k : ℝ)..y, A t * deriv ϕ t) - A x * ϕ x - (∫ t in (x : ℝ)..(m + 1), A t * deriv ϕ t) := ?_ + _ = A y * ϕ y - A x * ϕ x - ( + (∫ t in (x : ℝ)..(m + 1), A t * deriv ϕ t) + + (∫ t in (m + 1 : ℝ)..k, A t * deriv ϕ t) + + (∫ t in (k : ℝ)..y, A t * deriv ϕ t)) := ?_ _ = A y * ϕ y - A x * ϕ x - (∫ t in x..y, A t * deriv ϕ t) := ?_ · have h1 (n : ℕ) (hn : n ≠ 0) : A n - A (n - 1) = a n := by obtain ⟨n, rfl⟩ := exists_eq_succ_of_ne_zero hn @@ -118,7 +157,7 @@ lemma abel_summation {a : ArithmeticFunction ℝ} (x y : ℝ) (hx : 0 < x) (hxy · -- FTC-2 rw [← sum_neg_distrib] congr 2 - apply sum_congr rfl fun n hn => ?_ + apply sum_congr rfl fun n _ => ?_ rw [hint' n] · rw [neg_mul_eq_mul_neg, neg_sub] · intro z hz @@ -131,29 +170,16 @@ lemma abel_summation {a : ArithmeticFunction ℝ} (x y : ℝ) (hx : 0 < x) (hxy rwa [Nat.succ_le_iff] simp_rw [← Nat.cast_add_one] rw [intervalIntegral.sum_integral_adjacent_intervals_Ico this] - intro n hn - apply IntervalIntegrable.mul_continuousOn - · simp only [cast_add, cast_one, A] - rw [intervalIntegrable_iff_integrableOn_Ioo_of_le, IntegrableOn] - apply MeasureTheory.Integrable.congr (MeasureTheory.integrable_const (∑ j ∈ Iic n, a j)) - · simp only [measurableSet_Ioo, ae_restrict_eq] - rw [eventuallyEq_inf_principal_iff] - apply Eventually.of_forall - intro x hx - replace hx : ⌊x⌋₊ = n := by - simp only [Set.mem_Ioo] at hx - rw [Nat.floor_eq_iff (n.cast_nonneg.trans hx.1.le)] - exact ⟨hx.1.le, hx.2⟩ - simp [hx] - · rw [← Nat.cast_add_one, cast_le] - exact n.lt_add_one.le - · exact hϕ.continuous_deriv le_rfl |>.continuousOn + intro n _ + have hn := Nat.cast_le (α := ℝ).mpr n.lt_add_one.le + apply hIntervalIntegrable n _ _ hn + rw [Set.uIoc_of_le hn, Nat.cast_add_one] + exact Set.Ioc_subset_Icc_self · rw [hA x, hA y] have hy : ∫ t in ↑k..y, A t * deriv ϕ t = A k * (ϕ y - ϕ k) := by apply hint' intros z hz - have : k ≤ y := by simp [k, Nat.floor_le, (hx.trans hxy).le] - simp only [this, Set.uIoc_of_le, Set.mem_Ioc, floor_natCast, Set.mem_Icc, k] at hz ⊢ + simp only [hky, Set.uIoc_of_le, Set.mem_Ioc, floor_natCast, Set.mem_Icc, k] at hz ⊢ exact ⟨hz.1.le, hz.2.trans (Nat.lt_floor_add_one _).le⟩ have hx : ∫ t in x..m + 1, A t * deriv ϕ t = A x * (ϕ (m + 1) - ϕ x) := by apply hint' @@ -164,8 +190,53 @@ lemma abel_summation {a : ArithmeticFunction ℝ} (x y : ℝ) (hx : 0 < x) (hxy rw [hy, hx] simp only [k, m, hA x] ring - all_goals sorry -#exit + · ring + · have hab : IntervalIntegrable (fun t ↦ A t * deriv ϕ t) volume x (↑m + 1) := by + apply hIntervalIntegrable m _ _ (lt_floor_add_one x).le + simp only [(lt_floor_add_one x).le, Set.uIoc_of_le] + apply Set.Ioc_subset_Icc_self.trans + apply Set.Icc_subset_Icc_left (floor_le hx.le) + have hbc : IntervalIntegrable (fun t ↦ A t * deriv ϕ t) volume (↑m + 1) ↑k := by + rw [intervalIntegrable_iff_integrableOn_Ico_of_le] + swap + · norm_cast + have : Set.Ico (m + 1 : ℝ) k = ⋃ i ∈ Ico (m + 1) k, Set.Ico (i : ℝ) (i + 1) := by + ext n + simp only [Set.mem_Ico, mem_Ico, Set.mem_iUnion, Nat.lt_add_one_iff, exists_and_left, + exists_prop] + constructor + · rintro ⟨h1, h2⟩ + use ⌊n⌋₊ + have : 0 ≤ n := by + rw [← Nat.cast_add_one] at h1 + exact (Nat.cast_nonneg _).trans h1 + simp [Nat.floor_le, Nat.floor_lt, this, lt_floor_add_one, h2, le_floor, h1] + · rintro ⟨n', h⟩ + have : (m + 1 : ℝ) ≤ n' := by + rw [← Nat.cast_add_one, Nat.cast_le] + exact h.2.1.1 + refine ⟨this.trans h.1, h.2.2.trans_le ?_⟩ + rw [← Nat.cast_add_one, Nat.cast_le, Nat.add_one_le_iff] + exact h.2.1.2 + rw [this] + apply MeasureTheory.integrableOn_finset_iUnion.mpr + intro n _ + have hn' : (n : ℝ) ≤ n + 1 := by + rw [← Nat.cast_add_one, Nat.cast_le] + exact n.lt_add_one.le + apply hIntegrableOn n _ _ hn' + rw [Set.uIoc_of_le hn'] + exact Set.Ioc_subset_Icc_self + have hcd : IntervalIntegrable (fun t ↦ A t * deriv ϕ t) volume (↑k) y := by + apply hIntervalIntegrable k _ _ hky + simp only [hky, Set.uIoc_of_le] + apply Set.Ioc_subset_Icc_self.trans + refine Set.Icc_subset_Icc_right ?h.h + simp only [k, (lt_floor_add_one y).le] + rw [intervalIntegral.integral_add_adjacent_intervals hab hbc, + intervalIntegral.integral_add_adjacent_intervals (hab.trans hbc) hcd] + simp [A, intervalIntegral.integral_of_le hxy.le, MeasureTheory.integral_Icc_eq_integral_Ioc] + lemma nth_prime_one_eq_three : nth Nat.Prime 1 = 3 := nth_count prime_three @[simp] @@ -273,10 +344,9 @@ lemma th43_b (x : ℝ) (hx : 2 ≤ x) : -- fun_prop sorry - have h1 (r : ℝ) : ∑ p ∈ (Iic ⌊r⌋₊).filter Nat.Prime, Real.log p = - ∑ p ∈ (Iic ⌊r⌋₊), if p.Prime then Real.log p else 0 := by - rw [sum_filter] - -- simp_rw [h1] + -- have h1 (r : ℝ) : ∑ p ∈ (Iic ⌊r⌋₊).filter Nat.Prime, Real.log p = + -- ∑ p ∈ (Iic ⌊r⌋₊), if p.Prime then Real.log p else 0 := by + -- rw [sum_filter] let a : ArithmeticFunction ℝ := { toFun := Set.indicator (setOf Nat.Prime) (fun n => log n) map_zero' := by simp @@ -289,7 +359,6 @@ lemma th43_b (x : ℝ) (hx : 2 ≤ x) : refine log_ne_zero_of_pos_of_ne_one ?_ ?_ <;> norm_cast exacts [h.pos, h.ne_one] · rfl - -- stop have h2 := abel_summation (ϕ := fun x => (log x)⁻¹) (a := a) (3 / 2) x have h4 : ⌊(3/2 : ℝ)⌋₊ = 1 := by rw [@floor_div_ofNat]; rw [Nat.floor_ofNat] have h5 : Iic 1 = {0, 1} := by ext; simp; omega @@ -317,10 +386,15 @@ lemma th43_b (x : ℝ) (hx : 2 ≤ x) : rw [deriv_smoothingFn hu'] congr simp [div_eq_mul_inv, mul_comm] - simp [h3, h4, h5, h6, h7, h8, integral_neg] at h2 + have h9 : 3/2 < x := calc + 3/2 < 2 := by norm_num + _ ≤ x := hx + + simp [h3, h4, h5, h6, h7, h8, h9, integral_neg] at h2 rw [h2] simp [a, ← th_def', div_eq_mul_inv] - + rw [contDiff_one_iff_deriv] + sorry -- lemma th43_b' (x : ℝ) (hx : 2 ≤ x) : -- Nat.primeCounting ⌊x⌋₊ = From ada4727323fb7408a0aeab4a2a5fa2cb77e1a19d Mon Sep 17 00:00:00 2001 From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Sat, 28 Sep 2024 00:40:42 +0200 Subject: [PATCH 07/13] wip --- PrimeNumberTheoremAnd/Consequences.lean | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) diff --git a/PrimeNumberTheoremAnd/Consequences.lean b/PrimeNumberTheoremAnd/Consequences.lean index f538a6b1..a728fed8 100644 --- a/PrimeNumberTheoremAnd/Consequences.lean +++ b/PrimeNumberTheoremAnd/Consequences.lean @@ -12,7 +12,7 @@ open Finset open BigOperators Filter Real Classical Asymptotics MeasureTheory lemma abel_summation {a : ArithmeticFunction ℝ} (x y : ℝ) (hx : 0 < x) (hxy : x < y) - (ϕ : ℝ → ℝ) (hϕ : ContDiff ℝ 1 ϕ) : + (ϕ : ℝ → ℝ) (hϕ : ContDiffOn ℝ 1 ϕ (Set.Icc x y)) : ∑ n ∈ Ioc ⌊x⌋₊ ⌊y⌋₊, (a n : ℝ) * ϕ n = (∑ n ∈ Iic ⌊y⌋₊, a n) * ϕ y - (∑ n ∈ Iic ⌊x⌋₊, a n) * ϕ x - ∫ u in Set.Icc x y, (∑ n ∈ Iic ⌊u⌋₊, a n) * (deriv ϕ) u := by @@ -393,8 +393,15 @@ lemma th43_b (x : ℝ) (hx : 2 ≤ x) : simp [h3, h4, h5, h6, h7, h8, h9, integral_neg] at h2 rw [h2] simp [a, ← th_def', div_eq_mul_inv] - rw [contDiff_one_iff_deriv] - sorry + apply ContDiffOn.inv + apply ContDiffOn.log + apply contDiffOn_id + · intro z hz + simp at hz + linarith + · intro z hz + simp at hz + apply log_ne_zero_of_pos_of_ne_one <;> linarith -- lemma th43_b' (x : ℝ) (hx : 2 ≤ x) : -- Nat.primeCounting ⌊x⌋₊ = From 34909fb6975fa41d304cfbc5da3f01a6bd9a95e4 Mon Sep 17 00:00:00 2001 From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Sat, 28 Sep 2024 01:39:28 +0200 Subject: [PATCH 08/13] checkpoint --- PrimeNumberTheoremAnd/Consequences.lean | 76 +++++++++++++++++-------- 1 file changed, 51 insertions(+), 25 deletions(-) diff --git a/PrimeNumberTheoremAnd/Consequences.lean b/PrimeNumberTheoremAnd/Consequences.lean index a728fed8..cd81a7c1 100644 --- a/PrimeNumberTheoremAnd/Consequences.lean +++ b/PrimeNumberTheoremAnd/Consequences.lean @@ -12,10 +12,16 @@ open Finset open BigOperators Filter Real Classical Asymptotics MeasureTheory lemma abel_summation {a : ArithmeticFunction ℝ} (x y : ℝ) (hx : 0 < x) (hxy : x < y) - (ϕ : ℝ → ℝ) (hϕ : ContDiffOn ℝ 1 ϕ (Set.Icc x y)) : + (ϕ : ℝ → ℝ) -- (hϕ : ContDiffOn ℝ 1 ϕ (Set.Icc x y)) + (hϕ₁ : ∀ z ∈ Set.uIcc x y, DifferentiableAt ℝ ϕ z) + (hϕ₃ : ContinuousOn (deriv ϕ) (Set.Icc x y)) : ∑ n ∈ Ioc ⌊x⌋₊ ⌊y⌋₊, (a n : ℝ) * ϕ n = (∑ n ∈ Iic ⌊y⌋₊, a n) * ϕ y - (∑ n ∈ Iic ⌊x⌋₊, a n) * ϕ x - ∫ u in Set.Icc x y, (∑ n ∈ Iic ⌊u⌋₊, a n) * (deriv ϕ) u := by + have hϕ₂ : IntervalIntegrable (deriv ϕ) volume x y := (Set.uIcc_of_le hxy.le ▸ hϕ₃).intervalIntegrable + have le_add_one (n : ℕ) : (n : ℝ) ≤ n + 1 := by + rw [← Nat.cast_add_one, Nat.cast_le] + exact n.lt_add_one.le let m := ⌊x⌋₊ let k := ⌊y⌋₊ have hky : k ≤ y := by simp [k, Nat.floor_le, (hx.trans hxy).le] @@ -24,7 +30,7 @@ lemma abel_summation {a : ArithmeticFunction ℝ} (x y : ℝ) (hx : 0 < x) (hxy | inl hmk => simp only [m, k] at hmk rw [hmk,Ioc_self, sum_empty, ← mul_sub, eq_comm, sub_eq_zero, - ← intervalIntegral.integral_deriv_eq_sub, ← intervalIntegral.integral_const_mul, + ← intervalIntegral.integral_deriv_eq_sub hϕ₁ hϕ₂, ← intervalIntegral.integral_const_mul, intervalIntegral.integral_of_le hxy.le, integral_Ioc_eq_integral_Ioo, integral_Icc_eq_integral_Ioo] apply setIntegral_congr @@ -37,13 +43,11 @@ lemma abel_summation {a : ArithmeticFunction ℝ} (x y : ℝ) (hx : 0 < x) (hxy · rw [← hmk] exact Nat.floor_le_floor hz.1.le simp only [this] - · intros - exact hϕ.differentiable le_rfl |>.differentiableAt - · exact hϕ.continuous_deriv le_rfl |>.continuousOn |>.intervalIntegrable | inr hmk => let A (z : ℝ) := ∑ j ∈ Iic ⌊z⌋₊, a j have hA (z : ℝ) : A z = A ⌊z⌋₊ := by simp only [floor_natCast, A] - have hint' (a b : ℝ) (h : Set.uIoc a b ⊆ Set.Icc ⌊a⌋₊ (⌊a⌋₊ + 1)) : + have hint' (a b : ℝ) (hab : a ≤ b) (h : Set.Icc a b ⊆ Set.Icc ⌊a⌋₊ (⌊a⌋₊ + 1)) + (h' : Set.Icc (⌊a⌋₊ : ℝ) (⌊a⌋₊ + 1) ⊆ Set.Icc x y) : ∫ t in a..b, A t * deriv ϕ t = A a * (ϕ b - ϕ a) := by rw [← intervalIntegral.integral_deriv_eq_sub] · rw [← intervalIntegral.integral_const_mul] @@ -56,7 +60,8 @@ lemma abel_summation {a : ArithmeticFunction ℝ} (x y : ℝ) (hx : 0 < x) (hxy intro z hz simp only [mem_Ioo, Set.mem_compl_iff, Set.mem_setOf_eq, Classical.not_imp, not_or, Set.mem_singleton_iff] at hz ⊢ - have hz0 := h hz.1 + rw [Set.uIoc_of_le hab] at hz + have hz0 := Set.Ioc_subset_Icc_self.trans h hz.1 simp only [Set.mem_Icc] at hz0 apply hz0.2.eq_or_lt.resolve_right intro hz' @@ -65,14 +70,19 @@ lemma abel_summation {a : ArithmeticFunction ℝ} (x y : ℝ) (hx : 0 < x) (hxy exact ⟨hz0.1, hz'⟩ apply hz.2.1 simp only [← this, A, floor_natCast] - · intros - exact hϕ.differentiable le_rfl |>.differentiableAt - · exact hϕ.continuous_deriv le_rfl |>.continuousOn |>.intervalIntegrable - have hIntegrableOn (n : ℕ) (b c : ℝ) (hbc : b ≤ c) (h : Set.uIoc b c ⊆ Set.Icc n (n + 1)) : + · intros z hz + apply hϕ₁ + simp only [Set.uIcc_of_le, hxy.le, hab] at * + exact h.trans h' hz + · apply hϕ₂.mono_set + simp only [Set.uIcc_of_le, hxy.le, hab] at * + exact h.trans h' + have hIntegrableOn (n : ℕ) (b c : ℝ) (hbc : b ≤ c) (h : Set.uIoc b c ⊆ Set.Icc n (n + 1)) + (h' : Set.Icc (n : ℝ) (n + 1) ⊆ Set.Icc x y) : IntegrableOn (fun t ↦ A t * deriv ϕ t) (Set.Ico b c) volume := by obtain rfl | hbc := hbc.eq_or_lt · simp - have h' : Set.Icc b c ⊆ Set.Icc n (n + 1) := by + have h'' : Set.Icc b c ⊆ Set.Icc n (n + 1) := by rwa [← closure_Ioc hbc.ne, ← Set.uIoc_of_le hbc.le, isClosed_Icc.closure_subset_iff] apply IntegrableOn.mul_continuousOn_of_subset ?_ ?_ measurableSet_Ico CompactIccSpace.isCompact_Icc Set.Ico_subset_Icc_self @@ -84,7 +94,7 @@ lemma abel_summation {a : ArithmeticFunction ℝ} (x y : ℝ) (hx : 0 < x) (hxy apply Eventually.of_forall intro z hz replace hz : ⌊z⌋₊ = n := by - have := Set.Ico_subset_Icc_self.trans h' hz + have := Set.Ico_subset_Icc_self.trans h'' hz simp only [Set.mem_Icc] at this rw [Nat.floor_eq_iff (n.cast_nonneg.trans this.1)] refine ⟨this.1, ?_⟩ @@ -92,16 +102,16 @@ lemma abel_summation {a : ArithmeticFunction ℝ} (x y : ℝ) (hx : 0 < x) (hxy rintro rfl have : n + 1 < c := by simp only [Set.mem_Ico] at hz; exact hz.2 apply this.not_le - have := h' <| Set.right_mem_Icc.mpr hbc.le + have := h'' <| Set.right_mem_Icc.mpr hbc.le simp only [Set.mem_Icc] at this exact this.2 simp [hz] - · exact hϕ.continuous_deriv le_rfl |>.continuousOn - have hIntervalIntegrable (n : ℕ) (b c : ℝ) (hbc : b ≤ c) (h : Set.uIoc b c ⊆ Set.Icc n (n + 1)) : + · apply hϕ₃.mono (h''.trans h') + have hIntervalIntegrable (n : ℕ) (b c : ℝ) (hbc : b ≤ c) (h : Set.uIoc b c ⊆ Set.Icc n (n + 1)) + (h' : Set.Icc (n : ℝ) (n + 1) ⊆ Set.Icc x y) : IntervalIntegrable (fun t ↦ A t * deriv ϕ t) volume b c := by rw [intervalIntegrable_iff_integrableOn_Ico_of_le hbc] - apply hIntegrableOn n b c hbc h - + apply hIntegrableOn n b c hbc h h' calc _ = ∑ n ∈ Ioc m k, (A n - A (n - 1)) * ϕ n := ?_ _ = ∑ n ∈ Ioc m k, A n * ϕ n - ∑ n ∈ Ico m k, A n * ϕ (n + 1) := ?_ @@ -157,29 +167,45 @@ lemma abel_summation {a : ArithmeticFunction ℝ} (x y : ℝ) (hx : 0 < x) (hxy · -- FTC-2 rw [← sum_neg_distrib] congr 2 - apply sum_congr rfl fun n _ => ?_ + apply sum_congr rfl fun n hn => ?_ rw [hint' n] · rw [neg_mul_eq_mul_neg, neg_sub] + · exact le_add_one n · intro z hz simp only [le_add_iff_nonneg_right, zero_le_one, Set.uIoc_of_le, Set.mem_Ioc, floor_natCast, Set.mem_Icc] at hz ⊢ - exact ⟨hz.1.le, hz.2⟩ + exact ⟨hz.1, hz.2⟩ + · simp + intro z hz + simp at * + simp_rw [← Nat.add_one_le_iff, ← Nat.cast_le (α := ℝ), Nat.cast_add_one] at hn + exact ⟨(Nat.lt_floor_add_one x).le.trans hn.1 |>.trans hz.1, hz.2.trans hn.2 |>.trans hky⟩ · congr 2 rw [← Ico_succ_left] have : m.succ ≤ k := by rwa [Nat.succ_le_iff] simp_rw [← Nat.cast_add_one] rw [intervalIntegral.sum_integral_adjacent_intervals_Ico this] - intro n _ - have hn := Nat.cast_le (α := ℝ).mpr n.lt_add_one.le - apply hIntervalIntegrable n _ _ hn - rw [Set.uIoc_of_le hn, Nat.cast_add_one] - exact Set.Ioc_subset_Icc_self + intro n hn + have hn' := Nat.cast_le (α := ℝ).mpr n.lt_add_one.le + apply hIntervalIntegrable n _ _ hn' + · simp at hn + simp_rw [← Nat.add_one_le_iff, ← Nat.cast_le (α := ℝ), Nat.cast_add_one] at hn + apply Set.Icc_subset_Icc + · apply (Nat.lt_floor_add_one x).le.trans hn.1 + · apply hn.2.trans hky + · rw [Set.uIoc_of_le hn', Nat.cast_add_one] + exact Set.Ioc_subset_Icc_self · rw [hA x, hA y] have hy : ∫ t in ↑k..y, A t * deriv ϕ t = A k * (ϕ y - ϕ k) := by apply hint' intros z hz simp only [hky, Set.uIoc_of_le, Set.mem_Ioc, floor_natCast, Set.mem_Icc, k] at hz ⊢ + + · constructor + · apply le_trans ?_ hz.1 + + done exact ⟨hz.1.le, hz.2.trans (Nat.lt_floor_add_one _).le⟩ have hx : ∫ t in x..m + 1, A t * deriv ϕ t = A x * (ϕ (m + 1) - ϕ x) := by apply hint' From 202e9b094f41df91820112015c2343f34a11d2b2 Mon Sep 17 00:00:00 2001 From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Sat, 28 Sep 2024 02:24:12 +0200 Subject: [PATCH 09/13] wip --- PrimeNumberTheoremAnd/Consequences.lean | 119 ++++++++++++++++-------- 1 file changed, 78 insertions(+), 41 deletions(-) diff --git a/PrimeNumberTheoremAnd/Consequences.lean b/PrimeNumberTheoremAnd/Consequences.lean index cd81a7c1..4b35f16d 100644 --- a/PrimeNumberTheoremAnd/Consequences.lean +++ b/PrimeNumberTheoremAnd/Consequences.lean @@ -47,7 +47,7 @@ lemma abel_summation {a : ArithmeticFunction ℝ} (x y : ℝ) (hx : 0 < x) (hxy let A (z : ℝ) := ∑ j ∈ Iic ⌊z⌋₊, a j have hA (z : ℝ) : A z = A ⌊z⌋₊ := by simp only [floor_natCast, A] have hint' (a b : ℝ) (hab : a ≤ b) (h : Set.Icc a b ⊆ Set.Icc ⌊a⌋₊ (⌊a⌋₊ + 1)) - (h' : Set.Icc (⌊a⌋₊ : ℝ) (⌊a⌋₊ + 1) ⊆ Set.Icc x y) : + (h' : Set.Icc a b ⊆ Set.Icc x y) : ∫ t in a..b, A t * deriv ϕ t = A a * (ϕ b - ϕ a) := by rw [← intervalIntegral.integral_deriv_eq_sub] · rw [← intervalIntegral.integral_const_mul] @@ -73,12 +73,12 @@ lemma abel_summation {a : ArithmeticFunction ℝ} (x y : ℝ) (hx : 0 < x) (hxy · intros z hz apply hϕ₁ simp only [Set.uIcc_of_le, hxy.le, hab] at * - exact h.trans h' hz + exact h' hz · apply hϕ₂.mono_set simp only [Set.uIcc_of_le, hxy.le, hab] at * - exact h.trans h' + exact h' have hIntegrableOn (n : ℕ) (b c : ℝ) (hbc : b ≤ c) (h : Set.uIoc b c ⊆ Set.Icc n (n + 1)) - (h' : Set.Icc (n : ℝ) (n + 1) ⊆ Set.Icc x y) : + (h' : Set.Icc b c ⊆ Set.Icc x y) : IntegrableOn (fun t ↦ A t * deriv ϕ t) (Set.Ico b c) volume := by obtain rfl | hbc := hbc.eq_or_lt · simp @@ -106,9 +106,9 @@ lemma abel_summation {a : ArithmeticFunction ℝ} (x y : ℝ) (hx : 0 < x) (hxy simp only [Set.mem_Icc] at this exact this.2 simp [hz] - · apply hϕ₃.mono (h''.trans h') + · apply hϕ₃.mono h' have hIntervalIntegrable (n : ℕ) (b c : ℝ) (hbc : b ≤ c) (h : Set.uIoc b c ⊆ Set.Icc n (n + 1)) - (h' : Set.Icc (n : ℝ) (n + 1) ⊆ Set.Icc x y) : + (h' : Set.Icc b c ⊆ Set.Icc x y) : IntervalIntegrable (fun t ↦ A t * deriv ϕ t) volume b c := by rw [intervalIntegrable_iff_integrableOn_Ico_of_le hbc] apply hIntegrableOn n b c hbc h h' @@ -175,8 +175,7 @@ lemma abel_summation {a : ArithmeticFunction ℝ} (x y : ℝ) (hx : 0 < x) (hxy simp only [le_add_iff_nonneg_right, zero_le_one, Set.uIoc_of_le, Set.mem_Ioc, floor_natCast, Set.mem_Icc] at hz ⊢ exact ⟨hz.1, hz.2⟩ - · simp - intro z hz + · intro z hz simp at * simp_rw [← Nat.add_one_le_iff, ← Nat.cast_le (α := ℝ), Nat.cast_add_one] at hn exact ⟨(Nat.lt_floor_add_one x).le.trans hn.1 |>.trans hz.1, hz.2.trans hn.2 |>.trans hky⟩ @@ -189,39 +188,46 @@ lemma abel_summation {a : ArithmeticFunction ℝ} (x y : ℝ) (hx : 0 < x) (hxy intro n hn have hn' := Nat.cast_le (α := ℝ).mpr n.lt_add_one.le apply hIntervalIntegrable n _ _ hn' + · rw [Set.uIoc_of_le hn', Nat.cast_add_one] + exact Set.Ioc_subset_Icc_self · simp at hn simp_rw [← Nat.add_one_le_iff, ← Nat.cast_le (α := ℝ), Nat.cast_add_one] at hn apply Set.Icc_subset_Icc · apply (Nat.lt_floor_add_one x).le.trans hn.1 - · apply hn.2.trans hky - · rw [Set.uIoc_of_le hn', Nat.cast_add_one] - exact Set.Ioc_subset_Icc_self + · rw [Nat.cast_add_one] + apply hn.2.trans hky · rw [hA x, hA y] have hy : ∫ t in ↑k..y, A t * deriv ϕ t = A k * (ϕ y - ϕ k) := by apply hint' - intros z hz - simp only [hky, Set.uIoc_of_le, Set.mem_Ioc, floor_natCast, Set.mem_Icc, k] at hz ⊢ - - · constructor - · apply le_trans ?_ hz.1 - - done - exact ⟨hz.1.le, hz.2.trans (Nat.lt_floor_add_one _).le⟩ + · intros z hz + simp only [hky, Set.uIoc_of_le, Set.mem_Ioc, floor_natCast, Set.mem_Icc, k] at hz ⊢ + exact ⟨hz.1, hz.2.trans (Nat.lt_floor_add_one _).le⟩ + · apply Set.Icc_subset_Icc_left + rw [← Nat.add_one_le_iff, ← Nat.cast_le (α := ℝ), Nat.cast_add_one] at hmk + exact le_trans (Nat.lt_floor_add_one x).le hmk + · exact hky have hx : ∫ t in x..m + 1, A t * deriv ϕ t = A x * (ϕ (m + 1) - ϕ x) := by apply hint' - intros z hz - have : x ≤ m + 1 := by simp only [(Nat.lt_floor_add_one x).le, m] - simp only [this, Set.uIoc_of_le, Set.mem_Ioc, Set.mem_Icc, m] at hz ⊢ - refine ⟨(floor_le hx.le).trans hz.1.le, hz.2⟩ + · intros z hz + have : x ≤ m + 1 := by simp only [(Nat.lt_floor_add_one x).le, m] + simp only [this, Set.uIoc_of_le, Set.mem_Ioc, Set.mem_Icc, m] at hz ⊢ + refine ⟨(floor_le hx.le).trans hz.1, hz.2⟩ + · apply Set.Icc_subset_Icc_right + rw [← Nat.add_one_le_iff, ← Nat.cast_le (α := ℝ), Nat.cast_add_one] at hmk + exact hmk.trans hky + · exact (Nat.lt_floor_add_one x).le rw [hy, hx] simp only [k, m, hA x] ring · ring · have hab : IntervalIntegrable (fun t ↦ A t * deriv ϕ t) volume x (↑m + 1) := by apply hIntervalIntegrable m _ _ (lt_floor_add_one x).le - simp only [(lt_floor_add_one x).le, Set.uIoc_of_le] - apply Set.Ioc_subset_Icc_self.trans - apply Set.Icc_subset_Icc_left (floor_le hx.le) + · simp only [(lt_floor_add_one x).le, Set.uIoc_of_le] + apply Set.Ioc_subset_Icc_self.trans + apply Set.Icc_subset_Icc_left (floor_le hx.le) + · apply Set.Icc_subset_Icc_right + apply le_trans ?_ hky + norm_cast have hbc : IntervalIntegrable (fun t ↦ A t * deriv ϕ t) volume (↑m + 1) ↑k := by rw [intervalIntegrable_iff_integrableOn_Ico_of_le] swap @@ -246,19 +252,28 @@ lemma abel_summation {a : ArithmeticFunction ℝ} (x y : ℝ) (hx : 0 < x) (hxy exact h.2.1.2 rw [this] apply MeasureTheory.integrableOn_finset_iUnion.mpr - intro n _ + intro n hn have hn' : (n : ℝ) ≤ n + 1 := by rw [← Nat.cast_add_one, Nat.cast_le] exact n.lt_add_one.le apply hIntegrableOn n _ _ hn' - rw [Set.uIoc_of_le hn'] - exact Set.Ioc_subset_Icc_self + · rw [Set.uIoc_of_le hn'] + exact Set.Ioc_subset_Icc_self + · simp at hn + apply Set.Icc_subset_Icc + · rw [← Nat.cast_le (α := ℝ), Nat.cast_add_one] at hn + apply (Nat.lt_floor_add_one x).le.trans hn.1 + · rw [← Nat.add_one_le_iff, ← (n + 1).cast_le (α := ℝ), Nat.cast_add_one] at hn + apply hn.2.trans hky have hcd : IntervalIntegrable (fun t ↦ A t * deriv ϕ t) volume (↑k) y := by apply hIntervalIntegrable k _ _ hky - simp only [hky, Set.uIoc_of_le] - apply Set.Ioc_subset_Icc_self.trans - refine Set.Icc_subset_Icc_right ?h.h - simp only [k, (lt_floor_add_one y).le] + · simp only [hky, Set.uIoc_of_le] + apply Set.Ioc_subset_Icc_self.trans + refine Set.Icc_subset_Icc_right ?h.h + simp only [k, (lt_floor_add_one y).le] + · apply Set.Icc_subset_Icc_left + rw [← Nat.add_one_le_iff, ← Nat.cast_le (α := ℝ), Nat.cast_add_one] at hmk + exact le_trans (Nat.lt_floor_add_one x).le hmk rw [intervalIntegral.integral_add_adjacent_intervals hab hbc, intervalIntegral.integral_add_adjacent_intervals (hab.trans hbc) hcd] simp [A, intervalIntegral.integral_of_le hxy.le, MeasureTheory.integral_Icc_eq_integral_Ioc] @@ -419,15 +434,37 @@ lemma th43_b (x : ℝ) (hx : 2 ≤ x) : simp [h3, h4, h5, h6, h7, h8, h9, integral_neg] at h2 rw [h2] simp [a, ← th_def', div_eq_mul_inv] - apply ContDiffOn.inv - apply ContDiffOn.log - apply contDiffOn_id · intro z hz - simp at hz - linarith - · intro z hz - simp at hz - apply log_ne_zero_of_pos_of_ne_one <;> linarith + simp [h9.le] at hz + apply DifferentiableAt.inv + apply DifferentiableAt.log + apply differentiableAt_id' + · linarith + · apply log_ne_zero_of_pos_of_ne_one <;> linarith + · have : ∀ y ∈ Set.Icc (3 / 2) x, deriv (fun x ↦ (log x)⁻¹) y = -(y * log y ^ 2)⁻¹:= by + intro y hy + simp at hy + rw [deriv_smoothingFn, mul_inv, ← div_eq_mul_inv, neg_div] + linarith + intro z hz + apply ContinuousWithinAt.congr (f := fun x => - (x * log x ^ 2)⁻¹) + apply ContinuousWithinAt.neg + apply ContinuousWithinAt.inv₀ + apply ContinuousWithinAt.mul + apply continuousWithinAt_id + apply ContinuousWithinAt.pow + apply ContinuousWithinAt.log + apply continuousWithinAt_id + · simp [h9.le] at hz + linarith + · simp [h9.le] at hz + apply mul_ne_zero + · linarith + · apply pow_ne_zero + · apply log_ne_zero_of_pos_of_ne_one <;> linarith + · apply this + · apply this z hz + -- lemma th43_b' (x : ℝ) (hx : 2 ≤ x) : -- Nat.primeCounting ⌊x⌋₊ = From 43151134564bdaf247740087ba80ddf4c7b17d4a Mon Sep 17 00:00:00 2001 From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Sat, 28 Sep 2024 14:54:59 +0200 Subject: [PATCH 10/13] wip --- PrimeNumberTheoremAnd/Consequences.lean | 111 ++++++++++++++++++++---- 1 file changed, 96 insertions(+), 15 deletions(-) diff --git a/PrimeNumberTheoremAnd/Consequences.lean b/PrimeNumberTheoremAnd/Consequences.lean index 4b35f16d..2eadc458 100644 --- a/PrimeNumberTheoremAnd/Consequences.lean +++ b/PrimeNumberTheoremAnd/Consequences.lean @@ -94,9 +94,10 @@ lemma abel_summation {a : ArithmeticFunction ℝ} (x y : ℝ) (hx : 0 < x) (hxy apply Eventually.of_forall intro z hz replace hz : ⌊z⌋₊ = n := by + apply Nat.floor_eq_on_Ico + simp only [Set.mem_Ico] have := Set.Ico_subset_Icc_self.trans h'' hz simp only [Set.mem_Icc] at this - rw [Nat.floor_eq_iff (n.cast_nonneg.trans this.1)] refine ⟨this.1, ?_⟩ apply lt_of_le_of_ne this.2 rintro rfl @@ -350,6 +351,97 @@ lemma th_eq_zero_of_lt_two {x : ℝ} (hx : x < 2) : th x = 0 := by contrapose! this exact this.two_le +theorem extracted_2 (x : ℝ) (h9 : 3 / 2 < x) (z : ℝ) (hz : z ∈ Set.Icc (3 / 2) x) : + ContinuousWithinAt (fun x ↦ (x * log x ^ 2)⁻¹) (Set.Icc (3 / 2) x) z := by + apply ContinuousWithinAt.inv₀ + apply ContinuousWithinAt.mul + apply continuousWithinAt_id + apply ContinuousWithinAt.pow + apply ContinuousWithinAt.log + apply continuousWithinAt_id + · simp [h9.le] at hz + linarith + · simp [h9.le] at hz + apply mul_ne_zero + · linarith + · apply pow_ne_zero + · apply log_ne_zero_of_pos_of_ne_one <;> linarith + + +theorem extracted_1 (x : ℝ) (hx : 2 ≤ x) : + IntegrableOn + (fun t ↦ (∑ p ∈ filter Nat.Prime (Iic ⌊t⌋₊), log ↑p) / (t * log t ^ 2)) (Set.Icc 2 x) volume := by + have : 0 ≤ x := zero_le_two.trans hx + rw [Iic_eq_Icc, bot_eq_zero] + have : Set.Icc 2 x = Set.Ico (2 : ℝ) ⌊x⌋₊ ∪ Set.Icc (⌊x⌋₊ : ℝ) x := by + apply Set.Ico_union_Icc_eq_Icc .. |>.symm + · rwa [← Nat.cast_ofNat, Nat.cast_le, Nat.le_floor_iff this, Nat.cast_ofNat] + · exact floor_le this + rw [this] + apply IntegrableOn.union + swap + · apply IntegrableOn.mono_set (t := Set.Ico (⌊x⌋₊ : ℝ) (⌊x⌋₊ + 1)) + · simp_rw [div_eq_mul_inv] + apply IntegrableOn.mul_continuousOn_of_subset ?_ ?_ + measurableSet_Ico isCompact_Icc Set.Ico_subset_Icc_self + · change IntegrableOn (fun y => _) _ _ + apply Integrable.congr (integrable_const (∑ p ∈ filter Nat.Prime (Icc 0 ⌊x⌋₊), log p)) + simp only [measurableSet_Ico, ae_restrict_eq] + rw [eventuallyEq_inf_principal_iff] + apply Eventually.of_forall + intro z hz + replace hz := Nat.floor_eq_on_Ico _ _ hz + simp [hz] + + · intro z hz + apply ContinuousWithinAt.mono (extracted_2 _ _ _ _) + -- apply extracted_2 + all_goals sorry + · apply Set.Icc_subset_Ico_right + exact lt_floor_add_one x + + done + have : Set.Icc 2 x = ⋃ i ∈ Ico 2 ⌊x⌋₊, Set.Icc (i : ℝ) (i + 1) := by + ext y + by_cases hy : y < ↑⌊x⌋₊ + case neg => + simp at hy + simp + simp only [Set.mem_Ico, mem_Ico, Set.mem_iUnion, Nat.lt_add_one_iff, exists_and_left, + exists_prop] + simp only [Set.mem_Icc] + constructor + · rintro ⟨h1, h2⟩ + use ⌊y⌋₊ + have : 0 ≤ y := by + sorry + simp [Nat.floor_le, Nat.floor_lt, this, lt_floor_add_one, h2, le_floor, h1, le_of_lt] + + + · rintro ⟨n', h⟩ + have : (m + 1 : ℝ) ≤ n' := by + rw [← Nat.cast_add_one, Nat.cast_le] + exact h.2.1.1 + refine ⟨this.trans h.1, h.2.2.trans_le ?_⟩ + rw [← Nat.cast_add_one, Nat.cast_le, Nat.add_one_le_iff] + exact h.2.1.2 + rw [this] + apply MeasureTheory.integrableOn_finset_iUnion.mpr + intro n hn + have hn' : (n : ℝ) ≤ n + 1 := by + rw [← Nat.cast_add_one, Nat.cast_le] + exact n.lt_add_one.le + apply hIntegrableOn n _ _ hn' + · rw [Set.uIoc_of_le hn'] + exact Set.Ioc_subset_Icc_self + · simp at hn + apply Set.Icc_subset_Icc + · rw [← Nat.cast_le (α := ℝ), Nat.cast_add_one] at hn + apply (Nat.lt_floor_add_one x).le.trans hn.1 + · rw [← Nat.add_one_le_iff, ← (n + 1).cast_le (α := ℝ), Nat.cast_add_one] at hn + apply hn.2.trans hky + sorry + lemma th43_b (x : ℝ) (hx : 2 ≤ x) : Nat.primeCounting ⌊x⌋₊ = th x / log x + ∫ t in Set.Icc 2 x, th t / (t * (Real.log t) ^ 2) := by @@ -448,20 +540,9 @@ lemma th43_b (x : ℝ) (hx : 2 ≤ x) : linarith intro z hz apply ContinuousWithinAt.congr (f := fun x => - (x * log x ^ 2)⁻¹) - apply ContinuousWithinAt.neg - apply ContinuousWithinAt.inv₀ - apply ContinuousWithinAt.mul - apply continuousWithinAt_id - apply ContinuousWithinAt.pow - apply ContinuousWithinAt.log - apply continuousWithinAt_id - · simp [h9.le] at hz - linarith - · simp [h9.le] at hz - apply mul_ne_zero - · linarith - · apply pow_ne_zero - · apply log_ne_zero_of_pos_of_ne_one <;> linarith + · clear! a h4 h5 h6 h8 this hx + apply ContinuousWithinAt.neg + apply extracted_2 _ h9 _ hz · apply this · apply this z hz From 09141d83360bb1b347424bb7a94fed0caaf91838 Mon Sep 17 00:00:00 2001 From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Sat, 28 Sep 2024 20:32:07 +0200 Subject: [PATCH 11/13] finish and golf --- PrimeNumberTheoremAnd/Consequences.lean | 203 ++++++------------------ 1 file changed, 47 insertions(+), 156 deletions(-) diff --git a/PrimeNumberTheoremAnd/Consequences.lean b/PrimeNumberTheoremAnd/Consequences.lean index 2eadc458..fa4a2305 100644 --- a/PrimeNumberTheoremAnd/Consequences.lean +++ b/PrimeNumberTheoremAnd/Consequences.lean @@ -351,76 +351,64 @@ lemma th_eq_zero_of_lt_two {x : ℝ} (hx : x < 2) : th x = 0 := by contrapose! this exact this.two_le -theorem extracted_2 (x : ℝ) (h9 : 3 / 2 < x) (z : ℝ) (hz : z ∈ Set.Icc (3 / 2) x) : +theorem extracted_2 (x : ℝ) (z : ℝ) (hz_pos : 0 < z) (hz : z ≠ 1) : ContinuousWithinAt (fun x ↦ (x * log x ^ 2)⁻¹) (Set.Icc (3 / 2) x) z := by apply ContinuousWithinAt.inv₀ - apply ContinuousWithinAt.mul - apply continuousWithinAt_id - apply ContinuousWithinAt.pow - apply ContinuousWithinAt.log - apply continuousWithinAt_id - · simp [h9.le] at hz - linarith - · simp [h9.le] at hz - apply mul_ne_zero - · linarith - · apply pow_ne_zero - · apply log_ne_zero_of_pos_of_ne_one <;> linarith + · apply continuousWithinAt_id.mul <| (continuousWithinAt_id.log ?_).pow _ + simp [hz_pos.ne'] + · apply mul_ne_zero + · exact hz_pos.ne' + · apply pow_ne_zero _ <| log_ne_zero_of_pos_of_ne_one hz_pos hz theorem extracted_1 (x : ℝ) (hx : 2 ≤ x) : IntegrableOn (fun t ↦ (∑ p ∈ filter Nat.Prime (Iic ⌊t⌋₊), log ↑p) / (t * log t ^ 2)) (Set.Icc 2 x) volume := by - have : 0 ≤ x := zero_le_two.trans hx + have hx0 : 0 ≤ x := zero_le_two.trans hx + have hx2 : (2 : ℝ) ≤ ⌊x⌋₊ := by + rwa [← Nat.cast_ofNat, Nat.cast_le, Nat.le_floor_iff hx0, Nat.cast_ofNat] + have h (n : ℕ) (hn : 2 ≤ n) : + IntegrableOn (fun t ↦ (∑ p ∈ filter Nat.Prime (Icc 0 ⌊t⌋₊), log ↑p) / (t * log t ^ 2)) + (Set.Ico (n) (n + 1)) volume := by + have hn2 : (2 : ℝ) ≤ n := by norm_cast + have hn32 : (3 / 2 : ℝ) ≤ n := le_trans (by norm_num) hn2 + simp_rw [div_eq_mul_inv] + apply IntegrableOn.mul_continuousOn_of_subset ?_ ?_ + measurableSet_Ico isCompact_Icc Set.Ico_subset_Icc_self + · change IntegrableOn (fun y => _) _ _ + apply Integrable.congr (integrable_const (∑ p ∈ filter Nat.Prime (Icc 0 n), log p)) + simp only [measurableSet_Ico, ae_restrict_eq] + rw [eventuallyEq_inf_principal_iff] + apply Eventually.of_forall + intro z hz + replace hz := Nat.floor_eq_on_Ico _ _ hz + simp [hz] + · intro z hz + apply ContinuousWithinAt.mono (extracted_2 _ _ _ _) (Set.Icc_subset_Icc_left hn32) <;> + · simp only [Set.mem_Icc] at hz; linarith rw [Iic_eq_Icc, bot_eq_zero] - have : Set.Icc 2 x = Set.Ico (2 : ℝ) ⌊x⌋₊ ∪ Set.Icc (⌊x⌋₊ : ℝ) x := by - apply Set.Ico_union_Icc_eq_Icc .. |>.symm - · rwa [← Nat.cast_ofNat, Nat.cast_le, Nat.le_floor_iff this, Nat.cast_ofNat] - · exact floor_le this + have : Set.Icc 2 x = Set.Ico (2 : ℝ) ⌊x⌋₊ ∪ Set.Icc (⌊x⌋₊ : ℝ) x := + Set.Ico_union_Icc_eq_Icc hx2 (floor_le hx0) |>.symm rw [this] apply IntegrableOn.union swap · apply IntegrableOn.mono_set (t := Set.Ico (⌊x⌋₊ : ℝ) (⌊x⌋₊ + 1)) - · simp_rw [div_eq_mul_inv] - apply IntegrableOn.mul_continuousOn_of_subset ?_ ?_ - measurableSet_Ico isCompact_Icc Set.Ico_subset_Icc_self - · change IntegrableOn (fun y => _) _ _ - apply Integrable.congr (integrable_const (∑ p ∈ filter Nat.Prime (Icc 0 ⌊x⌋₊), log p)) - simp only [measurableSet_Ico, ae_restrict_eq] - rw [eventuallyEq_inf_principal_iff] - apply Eventually.of_forall - intro z hz - replace hz := Nat.floor_eq_on_Ico _ _ hz - simp [hz] - - · intro z hz - apply ContinuousWithinAt.mono (extracted_2 _ _ _ _) - -- apply extracted_2 - all_goals sorry + · apply h + exact_mod_cast hx2 · apply Set.Icc_subset_Ico_right exact lt_floor_add_one x - - done - have : Set.Icc 2 x = ⋃ i ∈ Ico 2 ⌊x⌋₊, Set.Icc (i : ℝ) (i + 1) := by + have : Set.Ico (2 : ℝ) ⌊x⌋₊ = ⋃ i ∈ Ico 2 ⌊x⌋₊, Set.Ico (i : ℝ) (i + 1) := by ext y - by_cases hy : y < ↑⌊x⌋₊ - case neg => - simp at hy - simp simp only [Set.mem_Ico, mem_Ico, Set.mem_iUnion, Nat.lt_add_one_iff, exists_and_left, exists_prop] - simp only [Set.mem_Icc] constructor · rintro ⟨h1, h2⟩ use ⌊y⌋₊ - have : 0 ≤ y := by - sorry + have : 0 ≤ y := zero_le_two.trans h1 simp [Nat.floor_le, Nat.floor_lt, this, lt_floor_add_one, h2, le_floor, h1, le_of_lt] - - · rintro ⟨n', h⟩ - have : (m + 1 : ℝ) ≤ n' := by - rw [← Nat.cast_add_one, Nat.cast_le] + have : (2 : ℝ) ≤ n' := by + rw [← Nat.cast_ofNat, Nat.cast_le] exact h.2.1.1 refine ⟨this.trans h.1, h.2.2.trans_le ?_⟩ rw [← Nat.cast_add_one, Nat.cast_le, Nat.add_one_le_iff] @@ -428,19 +416,8 @@ theorem extracted_1 (x : ℝ) (hx : 2 ≤ x) : rw [this] apply MeasureTheory.integrableOn_finset_iUnion.mpr intro n hn - have hn' : (n : ℝ) ≤ n + 1 := by - rw [← Nat.cast_add_one, Nat.cast_le] - exact n.lt_add_one.le - apply hIntegrableOn n _ _ hn' - · rw [Set.uIoc_of_le hn'] - exact Set.Ioc_subset_Icc_self - · simp at hn - apply Set.Icc_subset_Icc - · rw [← Nat.cast_le (α := ℝ), Nat.cast_add_one] at hn - apply (Nat.lt_floor_add_one x).le.trans hn.1 - · rw [← Nat.add_one_le_iff, ← (n + 1).cast_le (α := ℝ), Nat.cast_add_one] at hn - apply hn.2.trans hky - sorry + simp only [mem_Ico] at hn + apply h _ hn.1 lemma th43_b (x : ℝ) (hx : 2 ≤ x) : Nat.primeCounting ⌊x⌋₊ = @@ -474,12 +451,7 @@ lemma th43_b (x : ℝ) (hx : 2 ≤ x) : simp_all · exact measurableSet_Ico · unfold th - -- fun_prop - sorry - - -- have h1 (r : ℝ) : ∑ p ∈ (Iic ⌊r⌋₊).filter Nat.Prime, Real.log p = - -- ∑ p ∈ (Iic ⌊r⌋₊), if p.Prime then Real.log p else 0 := by - -- rw [sum_filter] + apply extracted_1 _ hx let a : ArithmeticFunction ℝ := { toFun := Set.indicator (setOf Nat.Prime) (fun n => log n) map_zero' := by simp @@ -535,56 +507,17 @@ lemma th43_b (x : ℝ) (hx : 2 ≤ x) : · apply log_ne_zero_of_pos_of_ne_one <;> linarith · have : ∀ y ∈ Set.Icc (3 / 2) x, deriv (fun x ↦ (log x)⁻¹) y = -(y * log y ^ 2)⁻¹:= by intro y hy - simp at hy + simp only [Set.mem_Icc] at hy rw [deriv_smoothingFn, mul_inv, ← div_eq_mul_inv, neg_div] linarith intro z hz apply ContinuousWithinAt.congr (f := fun x => - (x * log x ^ 2)⁻¹) - · clear! a h4 h5 h6 h8 this hx - apply ContinuousWithinAt.neg - apply extracted_2 _ h9 _ hz + · apply ContinuousWithinAt.neg + simp only [Set.mem_Icc] at hz + apply extracted_2 <;> linarith · apply this · apply this z hz - --- lemma th43_b' (x : ℝ) (hx : 2 ≤ x) : --- Nat.primeCounting ⌊x⌋₊ = --- (Real.log x)⁻¹ * ∑ p ∈ (Iic ⌊x⌋₊).filter Nat.Prime, Real.log p + --- ∫ t in Set.Icc 2 x, --- (∑ p ∈ (Iic ⌊t⌋₊).filter Nat.Prime, Real.log p) * (t * (Real.log t) ^ 2)⁻¹ := by --- have h1 (r : ℝ) : ∑ p ∈ (Iic ⌊r⌋₊).filter Nat.Prime, Real.log p = --- ∑ p ∈ (Iic ⌊r⌋₊), if p.Prime then Real.log p else 0 := by --- rw [sum_filter] --- -- simp_rw [h1] --- have h2 := abel_summation (ϕ := fun x => (log x)⁻¹) (a := ArithmeticFunction.primeCounting) (3 / 2) x --- simp [ArithmeticFunction.primeCounting] at h2 --- have : ⌊(3/2 : ℝ)⌋₊ = 1 := by rw [@floor_div_ofNat]; rw [Nat.floor_ofNat] --- simp [this] at h2 --- have : Iic 1 = {0, 1} := by ext; simp; omega --- simp [this] at h2 --- rw [eq_sub_iff_add_eq, add_comm, ← eq_sub_iff_add_eq] at h2 --- -- rw [← sub_mul] at h2 --- -- rw [← Finset.sum_sdiff_eq_sub] at h2 --- have := deriv_smoothingFn (one_lt_two.trans_le hx) --- have : --- ∫ (u : ℝ) in Set.Icc (3 / 2) x, (∑ x ∈ Iic ⌊u⌋₊, ↑x.primeCounting) * deriv (fun x ↦ (log x)⁻¹) u = --- ∫ (u : ℝ) in Set.Icc (3 / 2) x, (∑ x ∈ Iic ⌊u⌋₊, ↑x.primeCounting) * -(u * log u ^ 2)⁻¹ := by --- apply setIntegral_congr_ae --- · exact measurableSet_Icc --- refine Eventually.of_forall (fun u hu => ?_) --- have hu' : 1 < u := by --- simp at hu --- calc --- (1 : ℝ) < 3/2 := by norm_num --- _ ≤ u := hu.1 --- rw [deriv_smoothingFn hu'] --- congr --- simp [div_eq_mul_inv, mul_comm] --- simp [this, ← sum_mul] at h2 - - --- done --- #exit /-%% \begin{lemma}\label{range-eq-range}\lean{finsum_range_eq_sum_range, finsum_range_eq_sum_range'}\leanok For any arithmetic function $f$ and real number $x$, one has $$ \sum_{n \leq x} f(n) = \sum_{n \leq ⌊x⌋_+} f(n)$$ @@ -978,57 +911,15 @@ as $x \to \infty$. theorem pi_asymp : ∃ c : ℝ → ℝ, c =o[atTop] (fun _ ↦ (1:ℝ)) ∧ ∀ x : ℝ, Nat.primeCounting ⌊x⌋₊ = (1 + c x) * ∫ t in Set.Icc 2 x, 1 / (log t) ∂ volume := by - have h0 (x : ℝ) : - ∫ t in Set.Icc 2 x, - (∑ p ∈ (Iic ⌊t⌋₊).filter Nat.Prime, Real.log p) * (t * (Real.log t) ^ 2)⁻¹ = 0 := by - simp_rw [sum_mul] - convert - @MeasureTheory.integral_finset_sum - ℝ - _ - _ - _ - _ - (volume.restrict (Set.Icc (2 : ℝ) x)) - ℕ - ((Iic ⌊x⌋₊).filter Nat.Prime) - (fun i t => log ↑i * (t * log t ^ 2)⁻¹) - ?_ - using 1 - with u - done - have h1 (x : ℝ) : Nat.primeCounting ⌊x⌋₊ = + have h1 (x : ℝ) (hx : 2 ≤ x) : Nat.primeCounting ⌊x⌋₊ = (Real.log x)⁻¹ * ∑ p ∈ (Iic ⌊x⌋₊).filter Nat.Prime, Real.log p + ∫ t in Set.Icc 2 x, (∑ p ∈ (Iic ⌊t⌋₊).filter Nat.Prime, Real.log p) * (t * (Real.log t) ^ 2)⁻¹ := by -- can be proven by interchanging the sum and integral and using the fundamental theorem of -- calculus - simp_rw [sum_mul] - rw [@MeasureTheory.integral_finset_sum - ℝ - _ - _ - _ - _ - (volume.restrict (Set.Icc (2 : ℝ) x)) - ℕ - ((Iic ⌊x⌋₊).filter Nat.Prime) - fun i t => log ↑i * (t * log t ^ 2)⁻¹ - ] - - rw [← MeasureTheory.integral_subtype] - - rw [@MeasureTheory.integral_finset_sum - (Set.Icc 2 x) - _ - _ - _ - _ - volume - (ι := ℕ) (s := (Iic ⌊x⌋₊).filter Nat.Prime) - ] - sorry - #check chebyshev_asymptotic + rw [th43_b _ hx] + simp_rw [div_eq_mul_inv, th] + ring -- have h2 (ε : ℝ) : ∃ xε := chebyshev_asymptotic sorry From d2435dcd671f72038fe2a17d784975c35485c359 Mon Sep 17 00:00:00 2001 From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Sat, 28 Sep 2024 20:54:41 +0200 Subject: [PATCH 12/13] tidy --- PrimeNumberTheoremAnd/Consequences.lean | 51 +++++++++++++------------ 1 file changed, 26 insertions(+), 25 deletions(-) diff --git a/PrimeNumberTheoremAnd/Consequences.lean b/PrimeNumberTheoremAnd/Consequences.lean index fa4a2305..a25a02c2 100644 --- a/PrimeNumberTheoremAnd/Consequences.lean +++ b/PrimeNumberTheoremAnd/Consequences.lean @@ -11,8 +11,24 @@ open Nat hiding log open Finset open BigOperators Filter Real Classical Asymptotics MeasureTheory +lemma Set.Ico_subset_Ico_of_Icc_subset_Icc {a b c d : ℝ} (h : Set.Icc a b ⊆ Set.Icc c d) : + Set.Ico a b ⊆ Set.Ico c d := by + intro z hz + have hz' := Set.Ico_subset_Icc_self.trans h hz + have hcd : c ≤ d := by + contrapose! hz' + rw [Icc_eq_empty_of_lt hz'] + exact not_mem_empty _ + simp only [mem_Ico, mem_Icc] at * + refine ⟨hz'.1, hz'.2.eq_or_lt.resolve_left ?_⟩ + rintro rfl + apply hz.2.not_le + have := h <| right_mem_Icc.mpr (hz.1.trans hz.2.le) + simp only [mem_Icc] at this + exact this.2 + lemma abel_summation {a : ArithmeticFunction ℝ} (x y : ℝ) (hx : 0 < x) (hxy : x < y) - (ϕ : ℝ → ℝ) -- (hϕ : ContDiffOn ℝ 1 ϕ (Set.Icc x y)) + (ϕ : ℝ → ℝ) (hϕ₁ : ∀ z ∈ Set.uIcc x y, DifferentiableAt ℝ ϕ z) (hϕ₃ : ContinuousOn (deriv ϕ) (Set.Icc x y)) : ∑ n ∈ Ioc ⌊x⌋₊ ⌊y⌋₊, (a n : ℝ) * ϕ n = @@ -84,6 +100,7 @@ lemma abel_summation {a : ArithmeticFunction ℝ} (x y : ℝ) (hx : 0 < x) (hxy · simp have h'' : Set.Icc b c ⊆ Set.Icc n (n + 1) := by rwa [← closure_Ioc hbc.ne, ← Set.uIoc_of_le hbc.le, isClosed_Icc.closure_subset_iff] + have h'2 : Set.Ico b c ⊆ Set.Ico (n : ℝ) (n + 1) := Set.Ico_subset_Ico_of_Icc_subset_Icc h'' apply IntegrableOn.mul_continuousOn_of_subset ?_ ?_ measurableSet_Ico CompactIccSpace.isCompact_Icc Set.Ico_subset_Icc_self · simp only [cast_add, cast_one, A] @@ -93,19 +110,7 @@ lemma abel_summation {a : ArithmeticFunction ℝ} (x y : ℝ) (hx : 0 < x) (hxy rw [eventuallyEq_inf_principal_iff] apply Eventually.of_forall intro z hz - replace hz : ⌊z⌋₊ = n := by - apply Nat.floor_eq_on_Ico - simp only [Set.mem_Ico] - have := Set.Ico_subset_Icc_self.trans h'' hz - simp only [Set.mem_Icc] at this - refine ⟨this.1, ?_⟩ - apply lt_of_le_of_ne this.2 - rintro rfl - have : n + 1 < c := by simp only [Set.mem_Ico] at hz; exact hz.2 - apply this.not_le - have := h'' <| Set.right_mem_Icc.mpr hbc.le - simp only [Set.mem_Icc] at this - exact this.2 + replace hz : ⌊z⌋₊ = n := Nat.floor_eq_on_Ico _ _ (h'2 hz) simp [hz] · apply hϕ₃.mono h' have hIntervalIntegrable (n : ℕ) (b c : ℝ) (hbc : b ≤ c) (h : Set.uIoc b c ⊆ Set.Icc n (n + 1)) @@ -165,8 +170,7 @@ lemma abel_summation {a : ArithmeticFunction ℝ} (x y : ℝ) (hx : 0 < x) (hxy rw [sum_insert left_not_mem_Ioo, sum_insert right_not_mem_Ioo] simp_rw [mul_sub, sum_sub_distrib] abel - · -- FTC-2 - rw [← sum_neg_distrib] + · rw [← sum_neg_distrib] congr 2 apply sum_congr rfl fun n hn => ?_ rw [hint' n] @@ -363,7 +367,8 @@ theorem extracted_2 (x : ℝ) (z : ℝ) (hz_pos : 0 < z) (hz : z ≠ 1) : theorem extracted_1 (x : ℝ) (hx : 2 ≤ x) : IntegrableOn - (fun t ↦ (∑ p ∈ filter Nat.Prime (Iic ⌊t⌋₊), log ↑p) / (t * log t ^ 2)) (Set.Icc 2 x) volume := by + (fun t ↦ (∑ p ∈ filter Nat.Prime (Iic ⌊t⌋₊), log ↑p) / (t * log t ^ 2)) + (Set.Icc 2 x) volume := by have hx0 : 0 ≤ x := zero_le_two.trans hx have hx2 : (2 : ℝ) ≤ ⌊x⌋₊ := by rwa [← Nat.cast_ofNat, Nat.cast_le, Nat.le_floor_iff hx0, Nat.cast_ofNat] @@ -375,14 +380,12 @@ theorem extracted_1 (x : ℝ) (hx : 2 ≤ x) : simp_rw [div_eq_mul_inv] apply IntegrableOn.mul_continuousOn_of_subset ?_ ?_ measurableSet_Ico isCompact_Icc Set.Ico_subset_Icc_self - · change IntegrableOn (fun y => _) _ _ - apply Integrable.congr (integrable_const (∑ p ∈ filter Nat.Prime (Icc 0 n), log p)) + · apply Integrable.congr (integrable_const (∑ p ∈ filter Nat.Prime (Icc 0 n), log p)) simp only [measurableSet_Ico, ae_restrict_eq] rw [eventuallyEq_inf_principal_iff] apply Eventually.of_forall intro z hz - replace hz := Nat.floor_eq_on_Ico _ _ hz - simp [hz] + simp [Nat.floor_eq_on_Ico _ _ hz] · intro z hz apply ContinuousWithinAt.mono (extracted_2 _ _ _ _) (Set.Icc_subset_Icc_left hn32) <;> · simp only [Set.mem_Icc] at hz; linarith @@ -484,7 +487,7 @@ lemma th43_b (x : ℝ) (hx : 2 ≤ x) : · exact measurableSet_Icc refine Eventually.of_forall (fun u hu => ?_) have hu' : 1 < u := by - simp at hu + simp only [Set.mem_Icc] at hu calc (1 : ℝ) < 3/2 := by norm_num _ ≤ u := hu.1 @@ -500,9 +503,7 @@ lemma th43_b (x : ℝ) (hx : 2 ≤ x) : simp [a, ← th_def', div_eq_mul_inv] · intro z hz simp [h9.le] at hz - apply DifferentiableAt.inv - apply DifferentiableAt.log - apply differentiableAt_id' + refine (differentiableAt_id'.log ?_).inv ?_ · linarith · apply log_ne_zero_of_pos_of_ne_one <;> linarith · have : ∀ y ∈ Set.Icc (3 / 2) x, deriv (fun x ↦ (log x)⁻¹) y = -(y * log y ^ 2)⁻¹:= by From a788f212520e8581593c2203965f8488aa1b626a Mon Sep 17 00:00:00 2001 From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Sat, 28 Sep 2024 20:56:17 +0200 Subject: [PATCH 13/13] tidy --- PrimeNumberTheoremAnd/Consequences.lean | 3 --- 1 file changed, 3 deletions(-) diff --git a/PrimeNumberTheoremAnd/Consequences.lean b/PrimeNumberTheoremAnd/Consequences.lean index a25a02c2..ab7f6388 100644 --- a/PrimeNumberTheoremAnd/Consequences.lean +++ b/PrimeNumberTheoremAnd/Consequences.lean @@ -916,12 +916,9 @@ theorem pi_asymp : (Real.log x)⁻¹ * ∑ p ∈ (Iic ⌊x⌋₊).filter Nat.Prime, Real.log p + ∫ t in Set.Icc 2 x, (∑ p ∈ (Iic ⌊t⌋₊).filter Nat.Prime, Real.log p) * (t * (Real.log t) ^ 2)⁻¹ := by - -- can be proven by interchanging the sum and integral and using the fundamental theorem of - -- calculus rw [th43_b _ hx] simp_rw [div_eq_mul_inv, th] ring - -- have h2 (ε : ℝ) : ∃ xε := chebyshev_asymptotic sorry /-%%