diff --git a/PrimeNumberTheoremAnd/PerronFormula.lean b/PrimeNumberTheoremAnd/PerronFormula.lean
index e978c07..8c199d3 100644
--- a/PrimeNumberTheoremAnd/PerronFormula.lean
+++ b/PrimeNumberTheoremAnd/PerronFormula.lean
@@ -505,7 +505,7 @@ lemma isTheta (xpos : 0 < x) :
 /-%%
 \begin{lemma}[isIntegrable]\label{isIntegrable}\lean{Perron.isIntegrable}\leanok
 Let $x>0$ and $\sigma\in\R$. Then
-$$\int_{\R}\frac{x^{\sigma+it}}{(\sigma+it)(1+\sigma + it)}d\sigma$$
+$$\int_{\R}\frac{x^{\sigma+it}}{(\sigma+it)(1+\sigma + it)}dt$$
 is integrable.
 \end{lemma}
 %%-/
@@ -957,7 +957,7 @@ lemma formulaGtOne (x_gt_one : 1 < x) (σ_pos : 0 < σ) :
 \uses{isHolomorphicOn, residuePull1,
 residuePull2, contourPull3, integralPosAux, vertIntBoundLeft,
 tendsto_rpow_atTop_nhds_zero_of_norm_gt_one, limitOfConstantLeft}
-  Let $f(s) = x^s/(s(s+1))$. Then $f$ is holomorphic on $\C \setminus {0,1}$.
+  Let $f(s) = x^s/(s(s+1))$. Then $f$ is holomorphic on $\C \setminus {0,-1}$.
 %%-/
   set f : ℂ → ℂ := (fun s ↦ x^s / (s * (s + 1)))
 --%% First pull the contour from $(\sigma)$ to $(-1/2)$, picking up a residue $1$ at $s=0$.
diff --git a/PrimeNumberTheoremAnd/Wiener.lean b/PrimeNumberTheoremAnd/Wiener.lean
index e3d2da5..1b984ba 100644
--- a/PrimeNumberTheoremAnd/Wiener.lean
+++ b/PrimeNumberTheoremAnd/Wiener.lean
@@ -1709,7 +1709,7 @@ theorem wiener_ikehara_smooth_sub (h1 : Integrable Ψ) (hplus : closure (Functio
 
 /-%%
 \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
+  If $\Psi: (0,\infty) \to \C$ is smooth and compactly supported away from the origin, then,
 $$ \sum_{n=1}^\infty f(n) \Psi( \frac{n}{x} ) = A x \int_0^\infty \Psi(y)\ dy + o(x)$$
 as $x \to \infty$.
 \end{corollary}
@@ -2071,7 +2071,7 @@ lemma WienerIkeharaInterval_discrete' {f : ℕ → ℝ} (hpos : 0 ≤ f) (hf : 
 /-%%
 \begin{corollary}[Wiener-Ikehara theorem]\label{WienerIkehara}\lean{WienerIkeharaTheorem'}\leanok
   We have
-$$ \sum_{n\leq x} f(n) = A x |I|  + o(x).$$
+$$ \sum_{n\leq x} f(n) = A x + o(x).$$
 \end{corollary}
 %%-/
 
@@ -2294,7 +2294,7 @@ But observe that the quantity $\int_0^{Cx} \hat \psi( \frac{1}{2\pi}$ is non-neg
 /-%%
 \begin{corollary}[Wiener-Ikehara theorem, II]\label{WienerIkehara-alt}\lean{WienerIkeharaTheorem''}\leanok
   We have
-$$ \sum_{n\leq x} f(n) = A x |I|  + o(x).$$
+$$ \sum_{n\leq x} f(n) = A x + o(x).$$
 \end{corollary}
 %%-/