Fixing blueprint errors

Main.lean

@@ -0,0 +1,4 @@
+import «PrimeNumberTheoremAnd»
+
+def main : IO Unit :=
+  IO.println s!"Hello, {hello}!"

PrimeNumberTheoremAnd/Wiener.lean

@@ -260,7 +260,6 @@ lemma second_fourier {ψ : ℝ → ℂ} (hcont: Continuous ψ) (hsupp: HasCompac
     (x^(σ' - 1) : ℝ) * ∫ t, (1 / (σ' + t * I - 1)) * ψ t * x^(t * I) ∂ volume := by
 /-%%
 \begin{proof}\leanok
-\uses{first-fourier}
 The left-hand side expands as
 $$ \int_{-\log x}^\infty \int_\R e^{-u(\sigma-1)} \psi(t) e(-\frac{tu}{2\pi})\ dt\ du =
 x^{\sigma - 1} \int_\R \frac{1}{\sigma+it-1} \psi(t) x^{it}\ dt$$
@@ -355,7 +354,7 @@ lemma limiting_fourier {ψ:ℝ → ℂ} (hψ: ContDiff ℝ 2 ψ) (hsupp: HasComp
 %%-/
 
 /-%%
-\begin{corollary}\label{limiting-cor}\lean{limiting_cor}\leanok  With the hypotheses as above, we have
+\begin{corollary}[Corollary of limiting identity]\label{limiting-cor}\lean{limiting_cor}\leanok  With the hypotheses as above, we have
   $$ \sum_{n=1}^\infty \frac{f(n)}{n} \hat \psi( \frac{1}{2\pi} \log \frac{n}{x} ) = A \int_{-\infty}^\infty \hat \psi(\frac{u}{2\pi})\ du + o(1)$$
   as $x \to \infty$.
 \end{corollary}
@@ -373,16 +372,71 @@ lemma limiting_cor {ψ:ℝ → ℂ} (hψ: ContDiff ℝ 2 ψ) (hsupp: HasCompactS
 %%-/
 
 /-%%
-\begin{lemma}\label{schwarz-id}\lean{limiting_cor_schwartz}\leanok  The previous corollary also holds for functions $\psi$ that are assumed to be in the Schwartz class, as opposed to being $C^2$ and compactly supported.
+\begin{lemma}[Smooth Urysohn lemma]\label{smooth-ury}\lean{smooth_urysohn}\leanok  If $I$ is a closed interval contained in an open interval $J$, then there exists a smooth function $\Psi: \R \to \R$ with $1_I \leq \Psi \leq 1_J$.
+\end{lemma}
+%%-/
+
+lemma smooth_urysohn {a b c d:ℝ} (h1: a < b) (h2: b<c) (h3: c < d) : ∃ Ψ:ℝ → ℝ, (∀ n, ContDiff ℝ n Ψ) ∧ (HasCompactSupport Ψ) ∧ Set.indicator (Set.Icc b c) 1 ≤ Ψ ∧ Ψ ≤ Set.indicator (Set.Ioo a d) 1 := by
+  have := exists_smooth_zero_one_of_isClosed (modelWithCornersSelf ℝ ℝ) (s := Set.Iic a ∪ Set.Ici d) (t := Set.Icc b c)
+    (IsClosed.union isClosed_Iic isClosed_Ici)
+    (isClosed_Icc)
+    (by
+      simp_rw [Set.disjoint_union_left, Set.disjoint_iff, Set.subset_def, Set.mem_inter_iff, Set.mem_Iic, Set.mem_Icc,
+        Set.mem_empty_iff_false, and_imp, imp_false, not_le, Set.mem_Ici]
+      constructor <;> intros <;> linarith)
+  rcases this with ⟨⟨Ψ, hΨcontMDiff⟩, hΨ0, hΨ1, hΨ01⟩
+  simp only [Set.EqOn, Set.mem_setOf_eq, Set.mem_union, Set.mem_Iic, Set.mem_Ici,
+    ContMDiffMap.coeFn_mk, Pi.zero_apply, Set.mem_Icc, Pi.one_apply, and_imp] at *
+  use Ψ
+  constructor
+  · rw [contDiff_all_iff_nat, ←contDiff_top]
+    exact ContMDiff.contDiff hΨcontMDiff
+  · constructor
+    · rw [hasCompactSupport_def]
+      apply IsCompact.closure_of_subset (K := Set.Icc a d) isCompact_Icc
+      rw [Function.support_subset_iff]
+      intro x hx
+      contrapose! hx
+      simp only [Set.mem_Icc, not_and_or] at hx
+      apply hΨ0
+      by_contra! h'
+      cases' hx <;> linarith
+    · constructor
+      · intro x
+        rw [Set.indicator_apply]
+        split_ifs with h
+        simp only [Set.mem_Icc, Pi.one_apply] at *
+        rw [hΨ1 h.left h.right]
+        exact (hΨ01 x).left
+      · intro x
+        rw [Set.indicator_apply]
+        split_ifs with h
+        simp at *
+        exact (hΨ01 x).right
+        rw [hΨ0]
+        simp only [Set.mem_Ioo, not_and_or] at h
+        by_contra! h'
+        cases' h <;> linarith
+  done
+
+
+/-%%
+\begin{proof}  \leanok
+A standard analysis lemma, which can be proven by convolving $1_K$ with a smooth approximation to the identity for some interval $K$ between $I$ and $J$. Note that we have ``SmoothBumpFunction''s on smooth manifolds in Mathlib, so this shouldn't be too hard...
+\end{proof}
+%%-/
+
+/-%%
+\begin{lemma}[Limiting identity for Schwartz functions]\label{schwarz-id}\lean{limiting_cor_schwartz}\leanok  The previous corollary also holds for functions $\psi$ that are assumed to be in the Schwartz class, as opposed to being $C^2$ and compactly supported.
 \end{lemma}
 %%-/
 
 lemma limiting_cor_schwartz {ψ: SchwartzMap ℝ ℂ} : Tendsto (fun x : ℝ ↦ ∑' n, f n / n * fourierIntegral ψ (1/(2*π) * log (n/x)) - A * ∫ u in Set.Ici (-log x), fourierIntegral ψ (u / (2*π)) ∂ volume) atTop (nhds 0) := by sorry
 
 /-%%
 \begin{proof}
-\uses{limiting-cor}
-For any $R>1$, one can use a smooth cutoff function to write $\psi = \psi_{\leq R} + \psi_{>R}$, where $\psi_{\leq R}$ is $C^2$ (in fact smooth) and compactly supported (on $[-R,R]$), and $\psi_{>R}$ obeys bounds of the form
+\uses{limiting-cor, smooth-ury}
+For any $R>1$, one can use a smooth cutoff function (provided by Lemma \ref{smooth-ury} to write $\psi = \psi_{\leq R} + \psi_{>R}$, where $\psi_{\leq R}$ is $C^2$ (in fact smooth) and compactly supported (on $[-R,R]$), and $\psi_{>R}$ obeys bounds of the form
 $$ |\psi_{>R}(t)|, |\psi''_{>R}(t)| \ll R^{-1} / (1 + |t|^2) $$
 where the implied constants depend on $\psi$.  By Lemma \ref{decay} we then have
 $$ \hat \psi_{>R}(u) \ll R^{-1} / (1+|u|^2).$$
@@ -395,7 +449,7 @@ Combining the two estimates and letting $R$ be large, we obtain the claim.
 %%-/
 
 /-%%
-\begin{lemma}\label{bij}\lean{fourier_surjection_on_schwartz}\leanok  The Fourier transform is a bijection on the Schwartz class.
+\begin{lemma}[Bijectivity of Fourier transform]\label{bij}\lean{fourier_surjection_on_schwartz}\leanok  The Fourier transform is a bijection on the Schwartz class.
 \end{lemma}
 %%-/
 
@@ -412,7 +466,7 @@ It can be proved here by appealing to Mellin inversion, Theorem \ref{MellinInver
 %%-/
 
 /-%%
-\begin{corollary}\label{WienerIkeharaSmooth}\lean{wiener_ikehara_smooth}\leanok
+\begin{corollary}[Smoothed Wiener-Ikehara]\label{WienerIkeharaSmooth}\lean{wiener_ikehara_smooth}\leanok
   If $\Psi: (0,\infty) \to \C$ is smooth and compactly supported away from the origin, then, then
 $$ \sum_{n=1}^\infty f(n) \Psi( \frac{n}{x} ) = A x \int_0^\infty \Psi(y)\ dy + o(x)$$
 as $u \to \infty$.
@@ -432,65 +486,11 @@ and the claim follows from Lemma \ref{schwarz-id}.
 \end{proof}
 %%-/
 
-/-%%
-\begin{lemma}[Smooth Urysohn lemma]\label{smooth-ury}\lean{smooth_urysohn}\leanok  If $I$ is a closed interval contained in an open interval $J$, then there exists a smooth function $\Psi: \R \to \R$ with $1_I \leq \Psi \leq 1_J$.
-\end{lemma}
-%%-/
-
-lemma smooth_urysohn {a b c d:ℝ} (h1: a < b) (h2: b<c) (h3: c < d) : ∃ Ψ:ℝ → ℝ, (∀ n, ContDiff ℝ n Ψ) ∧ (HasCompactSupport Ψ) ∧ Set.indicator (Set.Icc b c) 1 ≤ Ψ ∧ Ψ ≤ Set.indicator (Set.Ioo a d) 1 := by
-  have := exists_smooth_zero_one_of_isClosed (modelWithCornersSelf ℝ ℝ) (s := Set.Iic a ∪ Set.Ici d) (t := Set.Icc b c)
-    (IsClosed.union isClosed_Iic isClosed_Ici)
-    (isClosed_Icc)
-    (by
-      simp_rw [Set.disjoint_union_left, Set.disjoint_iff, Set.subset_def, Set.mem_inter_iff, Set.mem_Iic, Set.mem_Icc,
-        Set.mem_empty_iff_false, and_imp, imp_false, not_le, Set.mem_Ici]
-      constructor <;> intros <;> linarith)
-  rcases this with ⟨⟨Ψ, hΨcontMDiff⟩, hΨ0, hΨ1, hΨ01⟩
-  simp only [Set.EqOn, Set.mem_setOf_eq, Set.mem_union, Set.mem_Iic, Set.mem_Ici,
-    ContMDiffMap.coeFn_mk, Pi.zero_apply, Set.mem_Icc, Pi.one_apply, and_imp] at *
-  use Ψ
-  constructor
-  · rw [contDiff_all_iff_nat, ←contDiff_top]
-    exact ContMDiff.contDiff hΨcontMDiff
-  · constructor
-    · rw [hasCompactSupport_def]
-      apply IsCompact.closure_of_subset (K := Set.Icc a d) isCompact_Icc
-      rw [Function.support_subset_iff]
-      intro x hx
-      contrapose! hx
-      simp only [Set.mem_Icc, not_and_or] at hx
-      apply hΨ0
-      by_contra! h'
-      cases' hx <;> linarith
-    · constructor
-      · intro x
-        rw [Set.indicator_apply]
-        split_ifs with h
-        simp only [Set.mem_Icc, Pi.one_apply] at *
-        rw [hΨ1 h.left h.right]
-        exact (hΨ01 x).left
-      · intro x
-        rw [Set.indicator_apply]
-        split_ifs with h
-        simp at *
-        exact (hΨ01 x).right
-        rw [hΨ0]
-        simp only [Set.mem_Ioo, not_and_or] at h
-        by_contra! h'
-        cases' h <;> linarith
-  done
-
-
-/-%%
-\begin{proof}  \leanok
-A standard analysis lemma, which can be proven by convolving $1_K$ with a smooth approximation to the identity for some interval $K$ between $I$ and $J$. Note that we have ``SmoothBumpFunction''s on smooth manifolds in Mathlib, so this shouldn't be too hard...
-\end{proof}
-%%-/
 
 /-%%
 Now we add the hypothesis that $f(n) \geq 0$ for all $n$.
 
-\begin{proposition}
+\begin{proposition}[Wiener-Ikehara in an interval]
 \label{WienerIkeharaInterval}\lean{WienerIkeharaInterval}\leanok
   For any closed interval $I \subset (0,+\infty)$, we have
   $$ \sum_{n=1}^\infty f(n) 1_I( \frac{n}{x} ) = A x |I|  + o(x).$$
@@ -510,7 +510,7 @@ lemma WienerIkeharaInterval (a b:ℝ) (ha: 0 < a) (hb: a < b) : Tendsto (fun x :
 %%-/
 
 /-%%
-\begin{corollary}\label{WienerIkehara}\lean{WienerIkeharaTheorem'}\leanok
+\begin{corollary}[Wiener-Ikehara theorem]\label{WienerIkehara}\lean{WienerIkeharaTheorem'}\leanok
   We have
 $$ \sum_{n\leq x} f(n) = A x |I|  + o(x).$$
 \end{corollary}