From 302873ac4622861228023ebc0b4e6776f306c795 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Thu, 30 May 2024 13:57:12 +0200 Subject: [PATCH 1/8] Update Wiener.lean --- PrimeNumberTheoremAnd/Wiener.lean | 22 ++++++++++++---------- 1 file changed, 12 insertions(+), 10 deletions(-) diff --git a/PrimeNumberTheoremAnd/Wiener.lean b/PrimeNumberTheoremAnd/Wiener.lean index ef017e99..f8ec4481 100644 --- a/PrimeNumberTheoremAnd/Wiener.lean +++ b/PrimeNumberTheoremAnd/Wiener.lean @@ -1140,7 +1140,7 @@ lemma gg_of_hh {x : ℝ} (hx : x ≠ 0) (i : ℝ) : gg x i = x⁻¹ * hh (1 / (2 field_simp [gg, hh] lemma gg_l1 {x : ℝ} (hx : 0 < x) (n : ℕ) : |gg x n| ≤ 1 / n := by - simp [gg_of_hh hx.ne.symm, abs_mul] + simp only [gg_of_hh hx.ne.symm, one_div, mul_inv_rev, abs_mul] apply mul_le_mul le_rfl (hh_le _ _ (by positivity)) (by positivity) (by positivity) |>.trans (le_of_eq ?_) simp [abs_inv, abs_eq_self.mpr hx.le] ; field_simp @@ -1227,7 +1227,7 @@ theorem sum_le_integral {x₀ : ℝ} {f : ℝ → ℝ} {n : ℕ} (hf : AntitoneO have l4 : IntervalIntegrable f volume x₀ (x₀ + 1) := by apply IntegrableOn.intervalIntegrable - simp + simp only [ge_iff_le, le_add_iff_nonneg_right, zero_le_one, uIcc_of_le] apply hfi.mono_set apply Icc_subset_Icc ; linarith ; simp have l5 x (hx : x ∈ Ioc x₀ (x₀ + 1)) : (fun x ↦ f (x₀ + 1)) x ≤ f x := by @@ -1254,11 +1254,11 @@ theorem sum_le_integral {x₀ : ℝ} {f : ℝ → ℝ} {n : ℕ} (hf : AntitoneO simp [add_comm _ x₀] at this ; rw [this] rw [intervalIntegral.integral_add_adjacent_intervals] · apply IntegrableOn.intervalIntegrable - simp + simp only [ge_iff_le, le_add_iff_nonneg_right, zero_le_one, uIcc_of_le] apply hfi.mono_set apply Icc_subset_Icc ; linarith ; simp · apply IntegrableOn.intervalIntegrable - simp + simp only [ge_iff_le, add_le_add_iff_left, le_add_iff_nonneg_left, Nat.cast_nonneg, uIcc_of_le] apply hfi.mono_set apply Icc_subset_Icc ; linarith ; simp @@ -1334,7 +1334,7 @@ lemma hh_integrable_aux (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : · convert_to IntegrableOn g' _ exact integrableOn_Ioi_deriv_of_nonneg k3 key k4 k1 · have := integral_Ioi_of_hasDerivAt_of_nonneg k3 key k4 k1 - simp [g₀, g'] at this ⊢ + simp only [mul_inv_rev, inv_div, mul_neg, ↓reduceIte, sub_neg_eq_add, g', g₀] at this ⊢ convert this using 1 ; field_simp ; ring lemma hh_integrable (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : @@ -1832,7 +1832,7 @@ lemma WI_summable {f : ℕ → ℝ} {g : ℝ → ℝ} (hg : HasCompactSupport g) Summable (fun n => f n * g (n / x)) := by obtain ⟨M, hM⟩ := hg.bddAbove.mono subset_closure apply summable_of_finite_support - simp ; apply Finite.inter_of_right ; rw [finite_iff_bddAbove] + simp only [Function.support_mul] ; apply Finite.inter_of_right ; rw [finite_iff_bddAbove] exact ⟨Nat.ceil (M * x), fun i hi => by simpa using Nat.ceil_mono ((div_le_iff hx).mp (hM hi))⟩ lemma WI_sum_le {f : ℕ → ℝ} {g₁ g₂ : ℝ → ℝ} (hf : 0 ≤ f) (hg : g₁ ≤ g₂) (hx : 0 < x) @@ -1856,7 +1856,8 @@ lemma WI_sum_Iab_le {f : ℕ → ℝ} (hpos : 0 ≤ f) {C : ℝ} (hcheby : cheby rw [tsum_eq_sum l1, div_le_iff hx, mul_assoc, mul_assoc] apply Finset.sum_le_sum l2 |>.trans have := hcheby ⌈b * x⌉₊ ; simp at this ; apply this.trans - have : 0 ≤ C := by have := hcheby 1 ; simp [cumsum] at this ; exact (abs_nonneg _).trans this + have : 0 ≤ C := by have := hcheby 1 ; simp only [cumsum, Finset.range_one, Complex.norm_eq_abs, + abs_ofReal, Finset.sum_singleton, Nat.cast_one, mul_one] at this ; exact (abs_nonneg _).trans this refine mul_le_mul_of_nonneg_left ?_ this apply (Nat.ceil_lt_add_one (by positivity)).le.trans linarith @@ -1891,7 +1892,7 @@ lemma WI_tendsto_aux (a b : ℝ) {A : ℝ} (hA : 0 < A) : intro x hx1 hx2 constructor · simpa [lt_div_iff' hA] - · simp [Real.dist_eq] at hx2 ⊢ + · simp only [Real.dist_eq, dist_zero_right, Real.norm_eq_abs] at hx2 ⊢ have : |x / A - (b - a)| = |x - A * (b - a)| / A := by rw [← abs_eq_self.mpr hA.le, ← abs_div, abs_eq_self.mpr hA.le] ; congr ; field_simp rwa [this, div_lt_iff' hA] @@ -1927,7 +1928,7 @@ theorem residue_nonneg {f : ℕ → ℝ} (hpos : 0 ≤ f) (h1.continuous.integrable_of_hasCompactSupport h2).integrableOn have r3 : Ico 1 2 ⊆ Function.support ψ := by intro x hx ; have := h4 x ; simp [hx] at this ⊢ ; linarith have r4 : Ico 1 2 ⊆ Function.support ψ ∩ Ioi 0 := by - simp [r3] ; apply Ico_subset_Icc_self.trans ; rw [Icc_subset_Ioi_iff] <;> linarith + simp only [subset_inter_iff, r3, true_and] ; apply Ico_subset_Icc_self.trans ; rw [Icc_subset_Ioi_iff] <;> linarith have r5 : 1 ≤ volume ((Function.support fun y ↦ ψ y) ∩ Ioi 0) := by convert volume.mono r4 ; norm_num simpa [setIntegral_pos_iff_support_of_nonneg_ae r1 r2] using zero_lt_one.trans_le r5 have := div_nonneg l3 l4.le ; field_simp at this ; exact this @@ -2097,7 +2098,8 @@ lemma tendsto_S_S_zero {f : ℕ → ℝ} (hpos : 0 ≤ f) (hcheby : cheby f) : have l2 : |cumsum f ⌈ε * ↑N⌉₊ / ↑N| ≤ C * ⌈ε * N⌉₊ / N := by have r1 := hC ⌈ε * N⌉₊ have r2 : 0 ≤ cumsum f ⌈ε * N⌉₊ := by apply cumsum_nonneg hpos - simp [abs_div, abs_eq_self.mpr r2, abs_eq_self.mpr (hpos _)] at r1 ⊢ + simp only [Complex.norm_eq_abs, abs_ofReal, abs_eq_self.mpr (hpos _), abs_div, + abs_eq_self.mpr r2, Nat.abs_cast, ge_iff_le] at r1 ⊢ apply div_le_div_of_nonneg_right r1 (by positivity) simpa [← S_sub_S h2.2] using l2.trans_lt h1 From 6694a75527af54b36c9263eec0b573c063594b2c Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Thu, 30 May 2024 13:57:18 +0200 Subject: [PATCH 2/8] Update ResidueCalcOnRectangles.lean --- PrimeNumberTheoremAnd/ResidueCalcOnRectangles.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/PrimeNumberTheoremAnd/ResidueCalcOnRectangles.lean b/PrimeNumberTheoremAnd/ResidueCalcOnRectangles.lean index 4e3ed2d6..0423ff06 100644 --- a/PrimeNumberTheoremAnd/ResidueCalcOnRectangles.lean +++ b/PrimeNumberTheoremAnd/ResidueCalcOnRectangles.lean @@ -467,8 +467,8 @@ lemma ResidueTheoremAtOrigin' {z w c : ℂ} (h1 : z.re < 0) (h2 : z.im < 0) (h3 theorem ResidueTheoremInRectangle (zRe_le_wRe : z.re ≤ w.re) (zIm_le_wIm : z.im ≤ w.im) (pInRectInterior : Rectangle z w ∈ 𝓝 p) : RectangleIntegral' (λ s => c / (s - p)) z w = c := by - simp [rectangle_mem_nhds_iff, mem_reProdIm, uIoo_of_le zRe_le_wRe, uIoo_of_le zIm_le_wIm] - at pInRectInterior + simp only [rectangle_mem_nhds_iff, uIoo_of_le zRe_le_wRe, uIoo_of_le zIm_le_wIm, mem_reProdIm, + mem_Ioo] at pInRectInterior rw [RectangleIntegral.translate', RectangleIntegral'] have : 1 / (2 * ↑π * I) * (2 * I * ↑π * c) = c := by field_simp [two_pi_I_ne_zero] ; ring rwa [ResidueTheoremAtOrigin'] ; all_goals { simp [*] } From 99a307031dbaf7d9bea82613a6f7caf8661492fe Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Thu, 30 May 2024 13:57:22 +0200 Subject: [PATCH 3/8] Update MellinCalculus.lean --- PrimeNumberTheoremAnd/MellinCalculus.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/PrimeNumberTheoremAnd/MellinCalculus.lean b/PrimeNumberTheoremAnd/MellinCalculus.lean index cbfec83d..d90e5c14 100644 --- a/PrimeNumberTheoremAnd/MellinCalculus.lean +++ b/PrimeNumberTheoremAnd/MellinCalculus.lean @@ -123,7 +123,7 @@ lemma IntervalIntegral.integral_eq_integral_of_support_subset_Icc {a b : ℝ} { ← integral_indicator measurableSet_Icc, indicator_eq_self.2 h] · by_cases hab2 : b = a · rw [hab2] at h ⊢ - simp [intervalIntegral.integral_same] + simp only [intervalIntegral.integral_same] simp only [Icc_self] at h have : ∫ (x : ℝ), f x ∂μ = ∫ (x : ℝ) in {a}, f x ∂μ := by rw [ ← integral_indicator (by simp), indicator_eq_self.2 h] From 96697d19ffcb785ffdca681e177999eb3c16b2ef Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Thu, 30 May 2024 13:57:25 +0200 Subject: [PATCH 4/8] Update BrunTitchmarsh.lean --- PrimeNumberTheoremAnd/BrunTitchmarsh.lean | 20 +++++++++++--------- 1 file changed, 11 insertions(+), 9 deletions(-) diff --git a/PrimeNumberTheoremAnd/BrunTitchmarsh.lean b/PrimeNumberTheoremAnd/BrunTitchmarsh.lean index 765a4615..b55703df 100644 --- a/PrimeNumberTheoremAnd/BrunTitchmarsh.lean +++ b/PrimeNumberTheoremAnd/BrunTitchmarsh.lean @@ -63,7 +63,7 @@ theorem primesBetween_subset : (Finset.Icc (Nat.ceil x) (Nat.floor (x+y))).filter (fun d => ∀ p:ℕ, p.Prime → p ≤ z → ¬p ∣ d) ∪ (Finset.Icc 1 (Nat.floor z)) := by intro p - simp + simp only [Finset.mem_filter, Finset.mem_Icc, Nat.ceil_le, Finset.mem_union, and_imp] intro hx hxy hp by_cases hpz : p ≤ z · right @@ -93,7 +93,7 @@ theorem primesBetween_le_siftedSum_add : rw[siftedSum_eq_card] gcongr rw[Nat.card_Icc] - simp + simp only [add_tsub_cancel_right] apply Nat.floor_le linarith @@ -130,7 +130,7 @@ theorem multSum_eq (d : ℕ) (hd : d ≠ 0): (primeInterSieve x y z hz).multSum d = ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) := by unfold Sieve.multSum rw[primeInterSieve] - simp + simp only [Finset.sum_boole, Nat.cast_inj] trans ↑(Finset.Ioc (Nat.ceil x - 1) (Nat.floor (x+y)) |>.filter (d ∣ ·) |>.card) · rw [←Nat.Icc_succ_left] congr @@ -152,7 +152,7 @@ theorem Nat.ceil_le_self_add_one (x : ℝ) (hx : 0 ≤ x) : Nat.ceil x ≤ x + 1 theorem floor_approx (x : ℝ) (hx : 0 ≤ x) : ∃ C, |C| ≤ 1 ∧ ↑((Nat.floor x)) = x + C := by use ↑(Nat.floor x) - x - simp + simp only [add_sub_cancel, and_true] rw[abs_le] constructor · simp only [neg_le_sub_iff_le_add] @@ -162,7 +162,7 @@ theorem floor_approx (x : ℝ) (hx : 0 ≤ x) : ∃ C, |C| ≤ 1 ∧ ↑((Nat.f theorem ceil_approx (x : ℝ) (hx : 0 ≤ x) : ∃ C, |C| ≤ 1 ∧ ↑((Nat.ceil x)) = x + C := by use ↑(Nat.ceil x) - x - simp + simp only [add_sub_cancel, and_true] rw[abs_le] constructor · simp only [neg_le_sub_iff_le_add] @@ -290,7 +290,7 @@ theorem tmp (N : ℕ) : ((Finset.range N).filter Nat.Prime).card ≤ 4 * (N / Re · norm_cast apply Finset.card_le_card intro n - simp + simp only [Finset.mem_filter, Finset.mem_range, and_imp] refine fun hnN hp ↦ ⟨by omega, hp⟩ rw [← primesBetween_one] by_cases hN : N = 0 @@ -451,7 +451,7 @@ theorem IsBigO.nat_Top_of_atTop (f g : ℕ → ℝ) (h : f =O[Filter.atTop] g) ( · simp [hg, h0] rw [← mul_inv_le_iff'] apply Finset.le_max' - simp + simp only [Finset.mem_insert, Finset.mem_image, Finset.mem_range] exact .inr ⟨n, by omega, rfl⟩ · simp [hg] @@ -535,7 +535,7 @@ theorem card_isPrimePow_isBigO : theorem card_range_filter_isPrimePow_le : ∃ C, ∀ N, ((Finset.range N).filter IsPrimePow).card ≤ C * (N / Real.log N) := by convert_to (fun N ↦ ((Finset.range N).filter IsPrimePow).card : ℕ → ℝ) =O[⊤] (fun N ↦ (N / Real.log N)) - · simp + · simp only [isBigO_top, RCLike.norm_natCast, norm_div, Real.norm_eq_abs] peel with C N by_cases hN : N = 0 · simp [hN] @@ -543,7 +543,9 @@ theorem card_range_filter_isPrimePow_le : ∃ C, ∀ N, ((Finset.range N).filter apply Real.log_nonneg norm_cast; omega apply IsBigO.nat_Top_of_atTop _ _ card_isPrimePow_isBigO - simp + simp only [div_eq_zero_iff, Nat.cast_eq_zero, Real.log_eq_zero, Nat.cast_eq_one, or_self_left, + Finset.card_eq_zero, forall_eq_or_imp, Finset.range_zero, Finset.filter_empty, Finset.range_one, + true_and] refine ⟨rfl, ?_⟩ intro a ha exfalso From ac9659cd42c45d000e9a5a4853de46633af8bf3e Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Thu, 30 May 2024 14:04:22 +0200 Subject: [PATCH 5/8] Update SelbergBounds.lean --- .../Mathlib/NumberTheory/Sieve/SelbergBounds.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/SelbergBounds.lean b/PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/SelbergBounds.lean index 0b5e4511..27a3cdca 100644 --- a/PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/SelbergBounds.lean +++ b/PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/SelbergBounds.lean @@ -477,7 +477,9 @@ theorem boundingSum_ge_sum (s : SelbergSieve) (hnu : s.nu = (ζ : ArithmeticFunc simp · intro p hpp _ rw[hnu] - simp + simp only [ArithmeticFunction.pdiv_apply, ArithmeticFunction.natCoe_apply, + ArithmeticFunction.zeta_apply, Nat.cast_ite, CharP.cast_eq_zero, Nat.cast_one, + ArithmeticFunction.id_apply] rw [if_neg, one_div] apply inv_lt_one; norm_cast exact hpp.one_lt From 57a41091d7a16e44781fb296f9cfd66ef4951bf9 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Thu, 30 May 2024 14:19:02 +0200 Subject: [PATCH 6/8] Update Wiener.lean --- PrimeNumberTheoremAnd/Wiener.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/PrimeNumberTheoremAnd/Wiener.lean b/PrimeNumberTheoremAnd/Wiener.lean index f8ec4481..27d1572a 100644 --- a/PrimeNumberTheoremAnd/Wiener.lean +++ b/PrimeNumberTheoremAnd/Wiener.lean @@ -75,7 +75,7 @@ lemma smooth_urysohn_support_Ioo (h1 : a < b) (h3: c < d) : rw [Set.indicator_apply] split_ifs with h · have : Ψ x ∈ Set.range Ψ := by simp only [Set.mem_range, exists_apply_eq_apply] - have : Ψ x ∈ Set.Icc 0 1 := by exact hΨrange this + have : Ψ x ∈ Set.Icc 0 1 := hΨrange this simpa using this.2 · simp only [Set.mem_Ioo, Pi.one_apply] at * simp only [not_and_or, not_lt] at h From a0d2d7c60ab1126d8579cf138ac592646aee103b Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Thu, 30 May 2024 14:19:11 +0200 Subject: [PATCH 7/8] Update MellinCalculus.lean --- PrimeNumberTheoremAnd/MellinCalculus.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/PrimeNumberTheoremAnd/MellinCalculus.lean b/PrimeNumberTheoremAnd/MellinCalculus.lean index d90e5c14..00d0be79 100644 --- a/PrimeNumberTheoremAnd/MellinCalculus.lean +++ b/PrimeNumberTheoremAnd/MellinCalculus.lean @@ -1274,7 +1274,7 @@ lemma Smooth1Properties_above_aux2 {x y ε : ℝ} (hε : ε ∈ Ioo 0 1) (hy : y · have : y ^ (1 / ε) ≤ y := by nth_rewrite 2 [← rpow_one y] exact rpow_le_rpow_of_exponent_ge ypos y1 (by linarith [one_lt_one_div εpos ε1]) - have pos : 0 < y ^ (1 / ε) := by apply rpow_pos_of_pos <| ypos + have pos : 0 < y ^ (1 / ε) := rpow_pos_of_pos ypos _ rw [ge_iff_le, div_le_iff, div_mul_eq_mul_div, le_div_iff', mul_comm] <;> try linarith · rw [ge_iff_le, le_div_iff <| ypos]; exact (mul_le_iff_le_one_right zero_lt_two).mpr y1 /-%% From 26ced91c6aa0806327bd9773db4b158c4d199fd8 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Thu, 30 May 2024 14:19:16 +0200 Subject: [PATCH 8/8] Update Basic.lean --- PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/Basic.lean b/PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/Basic.lean index 08a3236a..7fd237ae 100644 --- a/PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/Basic.lean +++ b/PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/Basic.lean @@ -115,7 +115,7 @@ theorem nu_pos_of_dvd_prodPrimes {d : ℕ} (hd : d ∣ P) : 0 < ν d := by 0 < ∏ p in d.primeFactors, ν p := by apply prod_pos intro p hpd - have hp_prime : p.Prime := by exact prime_of_mem_primeFactors hpd + have hp_prime : p.Prime := prime_of_mem_primeFactors hpd have hp_dvd : p ∣ P := (dvd_of_mem_primeFactors hpd).trans hd exact s.nu_pos_of_prime p hp_prime hp_dvd _ = ν d := s.nu_mult.prod_factors_of_mult ν (Squarefree.squarefree_of_dvd hd s.prodPrimes_squarefree)