adding primed versions for 2 pi i factors

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}.

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