Merge pull request #214 from ajirving/bump414

PrimeNumberTheoremAnd/Consequences.lean

@@ -579,7 +579,7 @@ lemma sum_von_mangoldt_as_double_sum (x : ℝ) (hx: 0 ≤ x) :
             . simp at hp'
               have : (k' = k ∧ p' = p) := by
                 have := eq_of_prime_pow_eq h1.prime hp'.2.prime h2 h
-                rw [<-this, pow_right_inj] at h
+                rw [<-this, pow_right_inj₀] at h
                 . exact ⟨ h.symm, this.symm ⟩
                 . exact Prime.pos h1
                 exact Nat.Prime.ne_one h1
@@ -738,7 +738,7 @@ Filter.Tendsto (fun x ↦ log x ^ b / x^a) Filter.atTop (nhds 0) := by
     have h1 : 1 ≤ log x := by
       rwa [le_log_iff_exp_le h0]
     rw [div_rpow _ (le_of_lt h0)]
-    . rw [div_le_div_right (rpow_pos_of_pos h0 _), <-rpow_natCast, <-rpow_mul (zero_le_one.trans h1)]
+    . rw [div_le_div_iff_of_pos_right (rpow_pos_of_pos h0 _), <-rpow_natCast, <-rpow_mul (zero_le_one.trans h1)]
       apply rpow_le_rpow_of_exponent_le h1
       rw [<-div_le_iff₀ ha]
       exact le_ceil _
@@ -1530,7 +1530,7 @@ theorem pi_asymp'' :
     have ineq (x : ℝ) (hx : 2 < x) :
         |const| / |∫ (t : ℝ) in Set.Icc 2 x, (log t)⁻¹| ≤
         |const| / ((x - 2) * (log x)⁻¹) := by
-      apply div_le_div
+      apply div_le_div₀
       · exact abs_nonneg _
       · rfl
       · apply mul_pos
@@ -1630,7 +1630,7 @@ theorem pi_asymp'' :
         |C ε hε| / (∫ (t : ℝ) in Set.Icc 2 x, (log t)⁻¹) := by
         apply _root_.add_le_add (h₂ := le_rfl)
         apply _root_.add_le_add (h₂ := le_rfl)
-        apply div_le_div
+        apply div_le_div₀
         · apply mul_nonneg <;> try apply mul_nonneg <;> try linarith
           norm_num; exact log_nonneg <| by linarith
         · exact ineq1 ε hε (1/2) (by linarith) x (by simpa using ⟨by linarith, by linarith, by linarith⟩)
@@ -1643,7 +1643,7 @@ theorem pi_asymp'' :
         |C ε hε| / (∫ (t : ℝ) in Set.Icc 2 x, (log t)⁻¹) := by
         apply _root_.add_le_add (h₂ := le_rfl)
         apply _root_.add_le_add (h₁ := le_rfl)
-        apply div_le_div
+        apply div_le_div₀
         · exact le_trans (abs_nonneg _) <|
             hD ε hε (1/2) (by linarith) x (by simpa using ⟨by linarith, by linarith, by linarith⟩)
           -- apply mul_nonneg <;> try apply mul_nonneg <;> try linarith
@@ -1676,7 +1676,7 @@ theorem pi_asymp'' :
       linarith
     _ ≤ (1/2) * ε + (|D ε hε (1/2) (by linarith)| + |C ε hε|) / (∫ (t : ℝ) in Set.Icc 2 x, (log t)⁻¹) := by
       apply _root_.add_le_add (h₁ := le_rfl)
-      apply div_le_div
+      apply div_le_div₀
       · apply add_nonneg <;> exact abs_nonneg _
       · apply _root_.add_le_add (h₂ := le_rfl); exact le_abs_self _
       · apply integral_log_inv_pos; linarith
@@ -1754,7 +1754,7 @@ lemma pi_alt_Oaux1 : ∃ c, ∀ᶠ (x : ℝ) in atTop,
       · intro x hx
         simp only [Set.mem_Icc] at hx
         rw [inv_le_inv₀]
-        · apply pow_le_pow_left
+        · apply pow_le_pow_left₀
           · apply log_nonneg (by linarith)
           · rw [log_le_log_iff] <;> linarith
         · apply pow_pos
@@ -1800,7 +1800,7 @@ lemma pi_alt_Oaux2 : ∃ c, ∀ᶠ (x : ℝ) in atTop,
       · intro x hx
         simp only [Set.mem_Icc] at hx
         rw [inv_le_inv₀]
-        · apply pow_le_pow_left
+        · apply pow_le_pow_left₀
           · apply log_nonneg (by linarith)
           · rw [log_le_log_iff] <;> linarith
         · apply pow_pos

PrimeNumberTheoremAnd/Fourier.lean

@@ -1,6 +1,6 @@
 import Mathlib.Analysis.Distribution.SchwartzSpace
 import Mathlib.MeasureTheory.Integral.IntegralEqImproper
-import Mathlib.Topology.ContinuousMap.Bounded
+import Mathlib.Topology.ContinuousMap.Bounded.Basic
 import Mathlib.Order.Filter.ZeroAndBoundedAtFilter
 import Mathlib.Analysis.Fourier.Inversion
 import Mathlib.Analysis.Fourier.FourierTransformDeriv

PrimeNumberTheoremAnd/GeneralMeromorphic.lean

@@ -10,7 +10,7 @@ open scoped Interval
 
 /-%%
 \begin{definition}\label{MeromorphicOnRectangle}\lean{MeromorphicOnRectangle}\leanok
-\uses{Rectangle, RectangleBorder, RectangleIntegral}
+\uses{RectangleBorder, RectangleIntegral}
 A function $f$ is Meromorphic on a rectangle with corners $z$ and $w$ if it is holomorphic off a
 (finite) set of poles, none of which are on the boundary of the rectangle.
 [Note: Might be overkill, can just work explicitly with the functions that arise. Of course would be nice to have the general theory as well...]

PrimeNumberTheoremAnd/Mathlib/Data/Nat/FinMulAntidiagonal.lean

@@ -306,7 +306,7 @@ private theorem f_surj {n : ℕ} (hn : n ≠ 0) :
     rw [mem_filter, Finset.mem_product] at hb
     refine ⟨?_, hn⟩
     · rw [Fin.prod_univ_three a]
-      unfold_let a
+      unfold a
       simp only [Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.head_cons, Matrix.cons_val_two,
         Matrix.tail_cons]
       rw [Nat.mul_div_cancel_left' (Nat.gcd_dvd_left _ _), ←hb.2, lcm,

PrimeNumberTheoremAnd/MediumPNT.lean

@@ -1,5 +1,4 @@
 import PrimeNumberTheoremAnd.ZetaBounds
-import EulerProducts.PNT
 import Mathlib.Algebra.Group.Support
 
 set_option lang.lemmaCmd true
@@ -386,7 +385,7 @@ X^{s}ds = \frac{X^{1}}{1}\mathcal{M}(\widetilde{1_{\epsilon}})(1)
 
 /-%%
 \begin{proof}
-\uses{ZeroFreeBox, Rectangle, RectangleBorder, RectangleIntegral, ResidueOfLogDerivative,
+\uses{ZeroFreeBox, RectangleBorder, RectangleIntegral, ResidueOfLogDerivative,
 MellinOfSmooth1a, MellinOfSmooth1b, MellinOfSmooth1c, MellinOfDeltaSpikeAt1,
 SmoothedChebyshevPull1}
 Residue calculus / the argument principle.

PrimeNumberTheoremAnd/MellinCalculus.lean

@@ -1,7 +1,10 @@
+import EulerProducts.Auxiliary
 import Mathlib.Analysis.MellinInversion
 import PrimeNumberTheoremAnd.PerronFormula
 import Mathlib.Algebra.GroupWithZero.Units.Basic
 
+open scoped ContDiff
+
 set_option lang.lemmaCmd true
 
 -- TODO: move near `MeasureTheory.setIntegral_prod`
@@ -651,9 +654,9 @@ $$
 
 attribute [- simp] one_div in
 
-lemma SmoothExistence : ∃ (Ψ : ℝ → ℝ), (ContDiff ℝ ⊤ Ψ) ∧ (∀ x, 0 ≤ Ψ x) ∧
+lemma SmoothExistence : ∃ (Ψ : ℝ → ℝ), (ContDiff ℝ ∞ Ψ) ∧ (∀ x, 0 ≤ Ψ x) ∧
     Ψ.support ⊆ Icc (1 / 2) 2 ∧ ∫ x in Ici 0, Ψ x / x = 1 := by
-  suffices h : ∃ (Ψ : ℝ → ℝ), (ContDiff ℝ ⊤ Ψ) ∧ (∀ x, 0 ≤ Ψ x) ∧
+  suffices h : ∃ (Ψ : ℝ → ℝ), (ContDiff ℝ ∞ Ψ) ∧ (∀ x, 0 ≤ Ψ x) ∧
       Ψ.support ⊆ Set.Icc (1 / 2) 2 ∧ 0 < ∫ x in Set.Ici 0, Ψ x / x by
     rcases h with ⟨Ψ, hΨ, hΨnonneg, hΨsupp, hΨpos⟩
     let c := (∫ x in Ici 0, Ψ x / x)

PrimeNumberTheoremAnd/PerronFormula.lean

@@ -492,7 +492,7 @@ theorem isTheta_uniformlyOn_uIcc {x : ℝ} (xpos : 0 < x) (σ' σ'' : ℝ) :
 
 theorem isTheta_uniformlyOn_uIoc {x : ℝ} (xpos : 0 < x) (σ' σ'' : ℝ) :
     (fun (σ, (y : ℝ)) ↦ f x (σ + y * I)) =Θ[𝓟 (uIoc σ' σ'') ×ˢ (atBot ⊔ atTop)]
-    fun (σ, y) ↦ 1 / y^2 := by
+    fun (_, y) ↦ 1 / y^2 := by
   refine (𝓟 (uIoc σ' σ'')).eq_or_neBot.casesOn (fun hbot ↦ by simp [hbot]) (fun _ ↦ ?_)
   haveI : NeBot (atBot (α := ℝ) ⊔ atTop) := sup_neBot.mpr (Or.inl atBot_neBot)
   exact (isTheta_uniformlyOn_uIcc xpos σ' σ'').mono (by simpa using Ioc_subset_Icc_self)
@@ -698,7 +698,7 @@ variable  {α β : Type*} [LinearOrder β] [NoMaxOrder β] [TopologicalSpace β]
 lemma _root_.Filter.Tendsto.eventually_bddAbove {f : α → β} (hf : Tendsto f l (𝓝 y)) :
     ∀ᶠ s in l.smallSets, BddAbove (f '' s) := by
   obtain ⟨y', hy'⟩ := exists_gt y
-  obtain ⟨s, hsl, hs⟩ := (eventually_le_of_tendsto_lt hy' hf).exists_mem
+  obtain ⟨s, hsl, hs⟩ := (Tendsto.eventually_le_const hy' hf).exists_mem
   simp_rw [Filter.eventually_smallSets, bddAbove_def]
   refine ⟨s, hsl, fun t ht ↦ ⟨y', fun y hy ↦ ?_⟩⟩
   obtain ⟨x, hxt, hxy⟩ := hy

PrimeNumberTheoremAnd/Rectangle.lean

@@ -11,14 +11,6 @@ variable {z w : ℂ} {c : ℝ}
 This files gathers definitions and basic properties about rectangles.
 %%-/
 
-/-%%
-\begin{definition}\label{Rectangle}\lean{Rectangle}\leanok
-A Rectangle has corners $z$ and $w \in \C$.
-\end{definition}
-%%-/
-/-- A `Rectangle` has corners `z` and `w`. -/
-def Rectangle (z w : ℂ) : Set ℂ := [[z.re, w.re]] ×ℂ [[z.im, w.im]]
-
 namespace Rectangle
 
 lemma symm : Rectangle z w = Rectangle w z := by
@@ -45,9 +37,6 @@ lemma Square_apply (p : ℂ) (cpos : c > 0) :
   rw [Square, Rectangle, uIcc_of_le (by simp; linarith), uIcc_of_le (by simp; linarith)]
   simp
 
--- From PR #9598
-/-- The preimage under `equivRealProd` of `s ×ˢ t` is `s ×ℂ t`. -/
-lemma preimage_equivRealProd_prod (s t : Set ℝ) : equivRealProd ⁻¹' (s ×ˢ t) = s ×ℂ t := rfl
 
 @[simp]
 theorem preimage_equivRealProdCLM_reProdIm (s t : Set ℝ) :
@@ -62,17 +51,6 @@ theorem ContinuousLinearEquiv.coe_toLinearEquiv_symm {R : Type*} {S : Type*} [Se
     ⇑e.toLinearEquiv.symm = e.symm :=
   rfl
 
--- From PR #9598
-/-- The inequality `s × t ⊆ s₁ × t₁` holds in `ℂ` iff it holds in `ℝ × ℝ`. -/
-lemma reProdIm_subset_iff {s s₁ t t₁ : Set ℝ} : s ×ℂ t ⊆ s₁ ×ℂ t₁ ↔ s ×ˢ t ⊆ s₁ ×ˢ t₁ := by
-  simp_rw [← preimage_equivRealProd_prod, equivRealProd.preimage_subset]
-
--- From PR #9598
-/-- If `s ⊆ s₁ ⊆ ℝ` and `t ⊆ t₁ ⊆ ℝ`, then `s × t ⊆ s₁ × t₁` in `ℂ`. -/
-lemma reProdIm_subset_iff' {s s₁ t t₁ : Set ℝ} :
-    s ×ℂ t ⊆ s₁ ×ℂ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅ :=
-  reProdIm_subset_iff.trans prod_subset_prod_iff
-
 /-- The axis-parallel complex rectangle with opposite corners `z` and `w` is complex product
   of two intervals, which is also the convex hull of the four corners. Golfed from mathlib4\#9598.-/
 lemma segment_reProdIm_segment_eq_convexHull (z w : ℂ) :
@@ -96,11 +74,6 @@ lemma mem_Rect {z w : ℂ} (zRe_lt_wRe : z.re ≤ w.re) (zIm_lt_wIm : z.im ≤ w
 lemma square_neg (p : ℂ) (c : ℝ) : Square p (-c) = Square p c := by
   simpa [Square] using Rectangle.symm
 
-def Set.uIoo {α : Type*} [Lattice α] (a b : α) : Set α := Ioo (a ⊓ b) (a ⊔ b)
-
-@[simp]
-theorem uIoo_of_le {α : Type*} [Lattice α] {a b : α} (h : a ≤ b) : Set.uIoo a b = Ioo a b := by
-  rw [uIoo, inf_eq_left.2 h, sup_eq_right.2 h]
 
 theorem Set.left_not_mem_uIoo {a b : ℝ} : a ∉ Set.uIoo a b :=
   fun ⟨h1, h2⟩ ↦ (left_lt_sup.mp h2) (le_of_not_le (inf_lt_left.mp h1))
@@ -191,20 +164,6 @@ lemma rectangle_mem_nhds_iff {z w p : ℂ} : Rectangle z w ∈ 𝓝 p ↔
     p ∈ (Set.uIoo z.re w.re) ×ℂ (Set.uIoo z.im w.im) := by
   simp_rw [← mem_interior_iff_mem_nhds, Rectangle, Complex.interior_reProdIm, uIoo, uIcc, interior_Icc]
 
-/-- A real segment `[a₁, a₂]` translated by `b * I` is the complex line segment.
-Golfed from mathlib\#9598.-/
-lemma horizontalSegment_eq (a₁ a₂ b : ℝ) :
-    (fun (x : ℝ) ↦ x + b * I) '' [[a₁, a₂]] = [[a₁, a₂]] ×ℂ {b} :=
-  Set.ext fun _ => ⟨fun hx ↦ hx.casesOn fun _ ⟨_, hx⟩ ↦ by simpa [← hx, reProdIm],
-    fun hx ↦ hx.casesOn (by simp_all [Complex.ext_iff])⟩
-
-/-- A vertical segment `[b₁, b₂]` translated by `a` is the complex line segment.
-Golfed from mathlib\#9598.-/
-lemma verticalSegment_eq (a b₁ b₂ : ℝ) :
-    (fun (y : ℝ) ↦ a + y * I) '' [[b₁, b₂]] = {a} ×ℂ [[b₁, b₂]] :=
-  Set.ext fun _ => ⟨fun hx ↦ hx.casesOn fun _ ⟨_, hx⟩ ↦ by simpa [← hx, reProdIm],
-    fun hx ↦ hx.casesOn (by simp_all [Complex.ext_iff])⟩
-
 lemma mapsTo_rectangle_left_re (z w : ℂ) :
     MapsTo (fun (y : ℝ) => ↑z.re + ↑y * I) [[z.im, w.im]] (Rectangle z w) :=
   fun _ hx ↦ ⟨by simp, by simp [hx]⟩

PrimeNumberTheoremAnd/Sobolev.lean

@@ -3,6 +3,7 @@ import Mathlib.Analysis.Distribution.SchwartzSpace
 import Mathlib.Order.Filter.ZeroAndBoundedAtFilter
 
 open Real Complex MeasureTheory Filter Topology BoundedContinuousFunction SchwartzMap  BigOperators
+open scoped ContDiff
 
 variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ}
 
@@ -26,10 +27,10 @@ section lemmas
 
 noncomputable def funscale {E : Type*} (g : ℝ → E) (R x : ℝ) : E := g (R⁻¹ • x)
 
-lemma contDiff_ofReal : ContDiff ℝ ⊤ ofReal := by
+lemma contDiff_ofReal : ContDiff ℝ ∞ ofReal := by
   have key x : HasDerivAt ofReal 1 x := hasDerivAt_id x |>.ofReal_comp
   have key' : deriv ofReal = fun _ => 1 := by ext x ; exact (key x).deriv
-  refine contDiff_top_iff_deriv.mpr ⟨fun x => (key x).differentiableAt, ?_⟩
+  refine contDiff_infty_iff_deriv.mpr ⟨fun x => (key x).differentiableAt, ?_⟩
   simpa [key'] using contDiff_const
 
 omit [NormedSpace ℝ E] in
@@ -46,7 +47,7 @@ variable {f : CS n E} {R x v : ℝ}
 instance : CoeFun (CS n E) (fun _ => ℝ → E) where coe := CS.toFun
 
 instance : Coe (CS n ℝ) (CS n ℂ) where coe f := ⟨fun x => f x,
-  contDiff_ofReal.of_le le_top |>.comp f.h1, f.h2.comp_left (g := ofReal) rfl⟩
+  contDiff_ofReal.of_le (mod_cast le_top) |>.comp f.h1, f.h2.comp_left (g := ofReal) rfl⟩
 
 def neg (f : CS n E) : CS n E where
   toFun := -f
@@ -67,7 +68,7 @@ lemma continuous (f : CS n E) : Continuous f := f.h1.continuous
 
 noncomputable def deriv (f : CS (n + 1) E) : CS n E where
   toFun := _root_.deriv f
-  h1 := (contDiff_succ_iff_deriv.mp f.h1).2
+  h1 := (contDiff_succ_iff_deriv.mp f.h1).2.2
   h2 := f.h2.deriv
 
 lemma hasDerivAt (f : CS (n + 1) E) (x : ℝ) : HasDerivAt f (f.deriv x) x :=
@@ -150,7 +151,7 @@ lemma iteratedDeriv_sub {f g : ℝ → E} (hf : ContDiff ℝ n f) (hg : ContDiff
 
 noncomputable def deriv (f : W1 (n + 1) E) : W1 n E where
   toFun := _root_.deriv f
-  smooth := contDiff_succ_iff_deriv.mp f.smooth |>.2
+  smooth := contDiff_succ_iff_deriv.mp f.smooth |>.2.2
   integrable k hk := by
     simpa [iteratedDeriv_succ'] using f.integrable (Nat.succ_le_succ hk)