bump mathlib

PrimeNumberTheoremAnd/BrunTitchmarsh.lean

@@ -21,7 +21,7 @@ noncomputable section
 namespace BrunTitchmarsh
 
 /- Sifting primes ≤ z from the interval [x, x+y] -/
-def primeInterSieve (x y z : ℝ) (hz : 1 ≤ z): SelbergSieve := {
+def primeInterSieve (x y z : ℝ) (hz : 1 ≤ z) : SelbergSieve where
   support := Finset.Icc (Nat.ceil x) (Nat.floor (x+y))
   prodPrimes := primorial (Nat.floor z)
   prodPrimes_squarefree := primorial_squarefree _
@@ -31,15 +31,16 @@ def primeInterSieve (x y z : ℝ) (hz : 1 ≤ z): SelbergSieve := {
   nu := (ζ : ArithmeticFunction ℝ).pdiv .id
   nu_mult := by arith_mult
   nu_pos_of_prime := fun p hp _ => by
-    simp[if_neg hp.ne_zero, Nat.pos_of_ne_zero hp.ne_zero]
+    simp [if_neg hp.ne_zero, Nat.pos_of_ne_zero hp.ne_zero]
   nu_lt_one_of_prime := fun p hp _ => by
-    simp[hp.ne_zero]
+    simp only [ArithmeticFunction.pdiv_apply, ArithmeticFunction.natCoe_apply,
+      ArithmeticFunction.zeta_apply, hp.ne_zero, ↓reduceIte, Nat.cast_one,
+      ArithmeticFunction.id_apply, one_div]
     apply inv_lt_one
     norm_cast
     exact hp.one_lt
   level := z
   one_le_level := hz
-}
 
 /- The number of primes in the interval [a, b] -/
 def primesBetween (a b : ℝ) : ℕ :=
@@ -79,11 +80,12 @@ theorem primesBetween_subset :
 theorem primesBetween_le_siftedSum_add :
     primesBetween x (x+y) ≤ (primeInterSieve x y z hz).siftedSum + z := by
   classical
-  trans ↑((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))).card
-  · rw[primesBetween]
+  trans ↑((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))).card
+  · rw [primesBetween]
     norm_cast
     apply Finset.card_le_card
-    apply primesBetween_subset _ _ _ hx
+    exact primesBetween_subset _ _ _ hz
   trans ↑((Finset.Icc (Nat.ceil x) (Nat.floor (x+y))).filter (fun d => ∀ p:ℕ, p.Prime → p ≤ z → ¬p ∣ d)).card
     + ↑(Finset.Icc 1 (Nat.floor z)).card
   · norm_cast
@@ -262,7 +264,7 @@ theorem primesBetween_le (hz : 1 < z) :
     · linarith
     apply one_le_pow_of_one_le _ _
     linarith [Real.log_nonneg (by linarith)]
-  linarith [siftedSum_le _ _ _ hx hy hz, primesBetween_le_siftedSum_add x y z hx (le_of_lt hz)]
+  linarith [siftedSum_le _ _ _ hx hy hz, primesBetween_le_siftedSum_add x y z hz.le]
 
 theorem primesBetween_one (n : ℕ) : primesBetween 1 n = ((Finset.range (n+1)).filter Nat.Prime).card := by
   rw [primesBetween]
@@ -318,7 +320,7 @@ theorem rpow_mul_rpow_log_isBigO_id_div_log (k : ℝ) {r : ℝ} (hr : r < 1) : (
     trans (N ^ (1 : ℝ) * (N ^ ((1-r)/2 : ℝ))⁻¹)
     · rw [← Real.rpow_add hN, ← Real.rpow_neg hN.le, ← Real.rpow_add hN]
       ring_nf
-    · rw [← Nat.cast_one, Real.rpow_nat_cast, pow_one]
+    · rw [← Nat.cast_one, Real.rpow_natCast, pow_one]
   _ =O[atTop] (fun N ↦ (N : ℝ) * (Real.log N)⁻¹) := by
     apply IsBigO.mul (isBigO_refl ..)
     apply IsBigO.inv_rev
@@ -336,7 +338,7 @@ theorem err_isBigO : (fun x ↦ (x ^ (1 / 2 : ℝ) * (1 + 1 / 2 * Real.log x) ^
       apply Real.isLittleO_const_log_atTop.isBigO.add ((isBigO_refl ..).const_mul_left ..) |>.pow
     _ =O[atTop] _ := by
       convert rpow_mul_rpow_log_isBigO_id_div_log 3 (?_) <;> norm_num
-      rw [← Real.rpow_nat_cast]
+      rw [← Real.rpow_natCast]
       norm_cast
 
 theorem card_range_filter_prime_isBigO : (fun N ↦ ((Finset.range N).filter Nat.Prime).card : ℕ → ℝ) =O[atTop] (fun N ↦ N / Real.log N) := calc
@@ -380,7 +382,7 @@ theorem prime_or_pow (N n : ℕ) (hnN : n < N) (hnprime : IsPrimePow n) :
     exact hpkn.symm
 
 example (a : ℝ) (n : ℕ) : a ^ n = a ^ (n : ℝ) := by
-  exact (Real.rpow_nat_cast a n).symm
+  exact (Real.rpow_natCast a n).symm
 
 theorem Nat.log_eq_floor_logb (b n : ℕ) (hb : 1 < b) : Nat.log b n = Nat.floor (Real.logb b n) := by
   by_cases hn : n = 0
@@ -400,7 +402,7 @@ theorem Nat.log_eq_floor_logb (b n : ℕ) (hb : 1 < b) : Nat.log b n = Nat.floor
   · apply Nat.le_log_of_pow_le hb
     exact_mod_cast calc
       (b:ℝ) ^ ⌊Real.logb ↑b ↑n⌋₊ ≤ (b : ℝ)^ (Real.logb b n) := by
-        rw [← Real.rpow_nat_cast]
+        rw [← Real.rpow_natCast]
         gcongr
         · norm_cast; omega
         apply Nat.floor_le hlogb_nonneg

PrimeNumberTheoremAnd/Consequences.lean

@@ -205,12 +205,10 @@ theorem sum_mobius_div_self_le (N : ℕ) : |∑ n in range N, μ n / (n : ℚ)|
   cases' N with N
   /- simple cases -/
   simp only [range_zero, sum_empty, abs_zero, zero_le_one]
-  by_cases hN : 1 ≤ N
-  swap
-  simp only [not_le, lt_one_iff] at hN
-  subst hN
-  simp only [reduceSucc, range_one, sum_singleton, ArithmeticFunction.map_zero, cast_zero,
-    EuclideanDomain.div_zero, abs_zero, zero_le_one]
+  by_cases hN : 1 ≤ N; swap
+  · simp only [not_le, lt_one_iff] at hN
+    subst hN
+    simp
   /- annoying case -/
   have h_sum : 1 = ∑ d in range (N + 1), (μ d : ℚ) * (N / d : ℕ) := by calc
     (1 : ℚ) = ∑ m in Icc 1 N, ∑ d in m.divisors, μ d := by
@@ -268,7 +266,7 @@ theorem sum_mobius_div_self_le (N : ℕ) : |∑ n in range N, μ n / (n : ℚ)|
   simp_rw [← mul_comm_div, sum_sub_distrib, ← sum_mul] at h_sum
   rw [eq_sub_iff_add_eq, eq_comm, ← eq_div_iff (by norm_num [Nat.pos_iff_ne_zero.mp hN])] at h_sum
 
-  rw [succ_eq_add_one, h_sum, abs_le]
+  rw [h_sum, abs_le]
   rw [abs_le, neg_sub] at h_bound
   constructor
   <;> simp only [le_div_iff, div_le_iff, cast_pos.mpr hN]

PrimeNumberTheoremAnd/Fourier.lean

@@ -3,8 +3,7 @@ import Mathlib.MeasureTheory.Integral.IntegralEqImproper
 import Mathlib.Topology.ContinuousFunction.Bounded
 import Mathlib.Order.Filter.ZeroAndBoundedAtFilter
 import Mathlib.Analysis.Fourier.Inversion
-
-import PrimeNumberTheoremAnd.Mathlib.Analysis.Fourier.FourierTransformDeriv
+import Mathlib.Analysis.Fourier.FourierTransformDeriv
 import PrimeNumberTheoremAnd.Sobolev
 
 open FourierTransform Real Complex MeasureTheory Filter Topology BoundedContinuousFunction SchwartzMap VectorFourier BigOperators
@@ -62,114 +61,3 @@ theorem fourierIntegral_self_add_deriv_deriv (f : W21) (u : ℝ) :
 
 @[simp] lemma deriv_ofReal : deriv ofReal' = fun _ => 1 := by
   ext x ; exact ((hasDerivAt_id x).ofReal_comp).deriv
-
-theorem bla (a : ℂ) (f : ℝ → ℂ) (n : ℕ) (hf : ContDiff ℝ n f) :
-    iteratedDeriv n (fun x ↦ a * x * f x) = fun x =>
-      a * x * iteratedDeriv n f x + n * a * iteratedDeriv (n - 1) f x := by
-
-  induction n with
-  | zero => simp
-  | succ n ih =>
-    have l0 : ContDiff ℝ n f := hf.of_succ
-    rw [iteratedDeriv_succ, ih l0] ; ext x
-    have l5 : ContDiff ℝ (↑(1 + n)) f := by convert hf using 1 ; simp ; ring
-    have l4 : DifferentiableAt ℝ (fun x ↦ iteratedDeriv n f x) x := by
-      have := ((l5.iterate_deriv' 1 n).differentiable le_rfl).differentiableAt (x := x)
-      simpa [iteratedDeriv_eq_iterate] using this
-    have l3 : DifferentiableAt ℝ (fun x ↦ a * ↑x) x := by
-      apply DifferentiableAt.const_mul
-      exact (contDiff_ofReal.differentiable le_top).differentiableAt
-    have l1 : DifferentiableAt ℝ (fun x ↦ a * ↑x * iteratedDeriv n f x) x := l3.mul l4
-    have l2 : DifferentiableAt ℝ (fun x ↦ ↑n * a * iteratedDeriv (n - 1) f x) x := by
-      apply DifferentiableAt.const_mul
-      apply l5.differentiable_iteratedDeriv
-      norm_cast ; exact Nat.sub_le _ _ |>.trans_lt (by simp)
-    simp [deriv_add l1 l2, deriv_mul l3 l4, ← iteratedDeriv_succ]
-    cases n <;> simp <;> ring
-
-noncomputable def MS (a : ℂ) (f : 𝓢(ℝ, ℂ)) : 𝓢(ℝ, ℂ) where
-  toFun x := a * x * f x
-  smooth' := contDiff_const.mul contDiff_ofReal |>.mul f.smooth'
-  decay' k n := by
-    simp only [norm_iteratedFDeriv_eq_norm_iteratedDeriv]
-    simp_rw [bla a f n <| f.smooth'.of_le le_top]
-    obtain ⟨C₁, hC₁⟩ := f.decay' (k + 1) n
-    obtain ⟨C₂, hC₂⟩ := f.decay' k (n - 1)
-    use ‖a‖ * C₁ + ‖a‖ * n * C₂ ; intro x
-    have l2 := norm_add_le (a * x * iteratedDeriv n f x) (n * a * iteratedDeriv (n - 1) f x)
-    have l3 : 0 ≤ ‖x‖ ^ k := by positivity
-    apply (mul_le_mul_of_nonneg_left l2 l3).trans ; rw [mul_add] ; apply add_le_add
-    · have : 0 ≤ ‖a‖ := by positivity
-      convert mul_le_mul_of_nonneg_left (hC₁ x) this using 1
-      simp [norm_iteratedFDeriv_eq_norm_iteratedDeriv, abs_eq_self.mpr pi_nonneg] ; ring_nf ; rfl
-    · have : 0 ≤ ‖a‖ * n := by positivity
-      convert mul_le_mul_of_nonneg_left (hC₂ x) this using 1
-      simp [norm_iteratedFDeriv_eq_norm_iteratedDeriv, abs_eq_self.mpr pi_nonneg] ; ring_nf ; rfl
-
-@[simp] lemma MS_apply (a : ℂ) (f : 𝓢(ℝ, ℂ)) (x : ℝ) : MS a f x = (a * x) • f x := rfl
-
-lemma MS_iterate (a : ℂ) (f : 𝓢(ℝ, ℂ)) (n : ℕ) : (MS a)^[n] f = fun x : ℝ => (a * x) ^ n • f x := by
-  induction n generalizing f with
-  | zero => simp
-  | succ n ih => ext x ; simp [ih, pow_succ] ; ring
-
-lemma fourierIntegral_decay_aux (f : ℝ → ℂ) (k : ℕ) (h1 : ContDiff ℝ k f)
-    (h2 : ∀ n ≤ k, Integrable (iteratedDeriv n f)) (x : ℝ) :
-    ‖(2 * π * I * x) ^ k • 𝓕 f x‖ ≤ (∫ y : ℝ, ‖iteratedDeriv k f y‖) := by
-  have l2 (x : ℝ) : (2 * π * I * x) ^ k • 𝓕 f x = 𝓕 (iteratedDeriv k f) x := by
-    simp [Real.fourierIntegral_iteratedDeriv h1 (fun n hn => h2 n <| Nat.cast_le.mp hn) le_rfl]
-  simpa only [l2] using Fourier.norm_fourierIntegral_le_integral_norm ..
-
-lemma iteratedDeriv_schwartz (f : 𝓢(ℝ, ℂ)) (n : ℕ) : iteratedDeriv n f = (SchwartzMap.derivCLM ℝ)^[n] f := by
-  induction n with
-  | zero => rfl
-  | succ n ih => rw [iteratedDeriv_succ, ih, Function.iterate_succ'] ; rfl
-
-theorem fourierIntegral_decay (f : 𝓢(ℝ, ℂ)) (k : ℕ) : ∃ C, ∀ (x : ℝ), ‖x‖ ^ k * ‖𝓕 f x‖ ≤ C := by
-  convert_to ∃ C, ∀ x : ℝ, ‖x ^ k * 𝓕 f x‖ ≤ C ; · simp
-  convert_to ∃ C, ∀ x : ℝ, ‖(2 * π * I * x) ^ k * 𝓕 f x‖ / (2 * π) ^ k ≤ C using 4
-  · field_simp [mul_pow, abs_eq_self.mpr pi_nonneg] ; ring
-  convert_to ∃ C, ∀ x : ℝ, ‖(2 * π * I * x) ^ k • 𝓕 f x‖ / (2 * π) ^ k ≤ C
-  use (∫ (y : ℝ), ‖iteratedDeriv k (⇑f) y‖) / (2 * π) ^ k ; intro x
-  have l1 : ∀ n ≤ k, Integrable (iteratedDeriv n f) volume := by
-    simp_rw [iteratedDeriv_schwartz] ; simp [SchwartzMap.integrable]
-  have := fourierIntegral_decay_aux f k (f.smooth'.of_le le_top) l1 x
-  apply div_le_div_of_nonneg_right this (by positivity)
-
-noncomputable def FS (f : 𝓢(ℝ, ℂ)) : 𝓢(ℝ, ℂ) where
-  toFun := 𝓕 f
-  smooth' := by
-    rw [contDiff_top] ; intro n
-    apply Real.contDiff_fourierIntegral ; intro k _
-    apply SchwartzMap.integrable_pow_mul
-  decay' := by
-    simp only [norm_iteratedFDeriv_eq_norm_iteratedDeriv]
-    intro k n
-    have l1 (k : ℕ) (_ : k ≤ (n : ℕ∞)) : Integrable (fun x ↦ x ^ k • f x) volume := by
-      convert_to Integrable ((MS 1)^[k] f) ; · simp [MS_iterate]
-      apply SchwartzMap.integrable
-    simp_rw [@Real.iteratedDeriv_fourierIntegral ℂ _ _ f n n l1 le_rfl]
-    convert_to ∃ C, ∀ (x : ℝ), ‖x‖ ^ k * ‖𝓕 ((MS (-2 * π * I))^[n] f) x‖ ≤ C ; · simp [MS_iterate]
-    apply fourierIntegral_decay
-
-@[simp] lemma FS_apply (f : 𝓢(ℝ, ℂ)) (x : ℝ) : FS f x = 𝓕 f x := rfl
-
-@[simp] lemma FS_toFun (f : 𝓢(ℝ, ℂ)) : ⇑(FS f) = 𝓕 f := rfl
-
-@[simp] lemma schwarz_reduce (f : ℝ → ℂ) h1 h2 x : SchwartzMap.mk f h1 h2 x = f x := rfl
-
-theorem fourierfourier {f : ℝ → ℂ} (hfi : Integrable f) (hfi' : Integrable (𝓕 f))
-    (hfc : Continuous f) (x : ℝ) :
-    𝓕 (𝓕 f) x = f (-x) := by
-  rw [← MeasureTheory.Integrable.fourier_inversion (v := -x) hfi hfi' hfc.continuousAt]
-  simp [fourierIntegralInv, Real.fourierIntegral, VectorFourier.fourierIntegral]
-
-lemma FS4 (f : 𝓢(ℝ, ℂ)) : FS^[4] f = f := by
-  have li0 : Integrable (⇑f) volume := f.integrable
-  have li1 : Integrable (𝓕 ⇑f) := (FS f).integrable
-  have li2 : Integrable (𝓕 (𝓕 ⇑f)) := (FS (FS f)).integrable
-  have li3 : Integrable (𝓕 (𝓕 (𝓕 ⇑f))) volume := (FS (FS (FS f))).integrable
-  have lc2 : Continuous (𝓕 (𝓕 ⇑f)) := (FS (FS f)).continuous
-  ext x ; change 𝓕 (𝓕 (𝓕 (𝓕 f))) x = f x
-  rw [fourierfourier li2 li3 lc2, fourierfourier li0 li1 f.continuous]
-  simp

PrimeNumberTheoremAnd/Mathlib/Analysis/Asymptotics/Asymptotics.lean

@@ -32,8 +32,8 @@ theorem isLittleO_const_id_atBot2 [LinearOrder F''] [NoMinOrder F''] [ClosedIicT
   (isLittleO_const_id_cocompact c).mono atBot_le_cocompact
 
 theorem _root_.Filter.Eventually.natCast {f : ℝ → Prop} (hf : ∀ᶠ x in atTop, f x) : ∀ᶠ n : ℕ in atTop, f n :=
-  tendsto_nat_cast_atTop_atTop.eventually hf
+  tendsto_natCast_atTop_atTop.eventually hf
 
 theorem IsBigO.natCast {f g : ℝ → E} (h : f =O[atTop] g) :
     (fun n : ℕ => f n) =O[atTop] fun n : ℕ => g n :=
-  h.comp_tendsto tendsto_nat_cast_atTop_atTop
+  h.comp_tendsto tendsto_natCast_atTop_atTop