From 5d5d1cd104b73a1f3d265ec1bbb92d55c96cbe0d Mon Sep 17 00:00:00 2001
From: AlexKontorovich <58564076+AlexKontorovich@users.noreply.github.com>
Date: Thu, 1 Feb 2024 11:07:35 -0500
Subject: [PATCH] adding primed versions for 2 pi i factors

---
 PrimeNumberTheoremAnd/MellinCalculus.lean          | 8 ++++----
 PrimeNumberTheoremAnd/ResidueCalcOnRectangles.lean | 7 +++++--
 2 files changed, 9 insertions(+), 6 deletions(-)

diff --git a/PrimeNumberTheoremAnd/MellinCalculus.lean b/PrimeNumberTheoremAnd/MellinCalculus.lean
index a51432ff..e605a5d8 100644
--- a/PrimeNumberTheoremAnd/MellinCalculus.lean
+++ b/PrimeNumberTheoremAnd/MellinCalculus.lean
@@ -24,15 +24,15 @@ It is very convenient to define integrals along vertical lines in the complex pl
 Let $f$ be a function from $\mathbb{C}$ to $\mathbb{C}$, and let $\sigma$ be a real number. Then we define
 $$\int_{(\sigma)}f(s)ds = \int_{\sigma-i\infty}^{\sigma+i\infty}f(s)ds.$$
 \end{definition}
-[Note: Better to define $\int_{(\sigma)}$ as $\frac1{2\pi i}\int_{\sigma-i\infty}^{\sigma+i\infty}$??
-There's a factor of $2\pi i$ in such contour integrals...]
 
-Attempt on 2/1/24: yes, add $1/(2\pi i)$ to the definition of ``VerticalIntegral''  and ``RectangleIntegral'' (below).
+We also have a version with a factor of $1/(2\pi i)$.
 %%-/
 
 noncomputable def VerticalIntegral (f : ℂ → ℂ) (σ : ℝ) : ℂ :=
-  (1 / (2 * π)) * ∫ t : ℝ, f (σ + t * I)
+  I • ∫ t : ℝ, f (σ + t * I)
 
+noncomputable abbrev VerticalIntegral' (f : ℂ → ℂ) (σ : ℝ) : ℂ :=
+  (1 / (2 * π * I)) * ∫ t : ℝ, f (σ + t * I)
 
 /-%%
 The following is preparatory material used in the proof of the Perron formula, see Lemma \ref{PerronFormula}.
diff --git a/PrimeNumberTheoremAnd/ResidueCalcOnRectangles.lean b/PrimeNumberTheoremAnd/ResidueCalcOnRectangles.lean
index ba142bce..ebebebcc 100644
--- a/PrimeNumberTheoremAnd/ResidueCalcOnRectangles.lean
+++ b/PrimeNumberTheoremAnd/ResidueCalcOnRectangles.lean
@@ -24,15 +24,18 @@ def Rectangle (z w : ℂ) : Set ℂ := [[z.re, w.re]] ×ℂ [[z.im, w.im]]
 /-%%
 \begin{definition}\label{RectangleIntegral}\lean{RectangleIntegral}\leanok
 A RectangleIntegral of a function $f$ is one over a rectangle determined by $z$ and $w$ in $\C$.
-We will sometimes denote it by $\int_{z}^{w} f$.
+We will sometimes denote it by $\int_{z}^{w} f$. (There is also a primed version, which is $1/(2\pi i)$ times the original.)
 \end{definition}
 %%-/
 /-- A `RectangleIntegral` of a function `f` is one over a rectangle determined by
   `z` and `w` in `ℂ`. -/
 noncomputable def RectangleIntegral (f : ℂ → ℂ) (z w : ℂ) : ℂ :=
-    (1/(2 * π * I)) * ((∫ x : ℝ in z.re..w.re, f (x + z.im * I)) - (∫ x : ℝ in z.re..w.re, f (x + w.im * I))
+    ((∫ x : ℝ in z.re..w.re, f (x + z.im * I)) - (∫ x : ℝ in z.re..w.re, f (x + w.im * I))
      + I • (∫ y : ℝ in z.im..w.im, f (w.re + y * I)) - I • ∫ y : ℝ in z.im..w.im, f (z.re + y * I))
 
+noncomputable abbrev RectangleIntegral' (f : ℂ → ℂ) (z w : ℂ) : ℂ :=
+    (1/(2 * π * I)) * RectangleIntegral f z w
+
 /-- A function is `HolomorphicOn` a set if it is complex differentiable on that set. -/
 abbrev HolomorphicOn (f : ℂ → ℂ) (s : Set ℂ) : Prop := DifferentiableOn ℂ f s