Adapted from PNT+ by Alex Kontorovich and Terence Tao: ResidueCalcOnRectangles.lean, commit be5e07e04cde20c5ceabf63759bd097a9c88173f (Apache-2.0).

noncomputable def NumberField.Odlyzko.horizontalIntegral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (x₁ x₂ y : ℝ) : E

A horizontal integral used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.horizontalIntegral f x₁ x₂ y = ∫ (x : ℝ) in x₁..x₂, f (↑x + ↑y * Complex.I)

noncomputable def NumberField.Odlyzko.verticalSegmentIntegral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (x y₁ y₂ : ℝ) : E

A vertical segment integral used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.verticalSegmentIntegral f x y₁ y₂ = Complex.I • ∫ (y : ℝ) in y₁..y₂, f (↑x + ↑y * Complex.I)

noncomputable def NumberField.Odlyzko.rectangleIntegral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (z w : ℂ) : E

A rectangle integral used in the Odlyzko-bound argument.

Equations

• One or more equations did not get rendered due to their size.

theorem NumberField.Odlyzko.rectangleIntegral_congr {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f g : ℂ → E} {z w : ℂ} (hbottom : ∀ x ∈ Set.uIcc z.re w.re, f (↑x + ↑z.im * Complex.I) = g (↑x + ↑z.im * Complex.I)) (htop : ∀ x ∈ Set.uIcc z.re w.re, f (↑x + ↑w.im * Complex.I) = g (↑x + ↑w.im * Complex.I)) (hright : ∀ y ∈ Set.uIcc z.im w.im, f (↑w.re + ↑y * Complex.I) = g (↑w.re + ↑y * Complex.I)) (hleft : ∀ y ∈ Set.uIcc z.im w.im, f (↑z.re + ↑y * Complex.I) = g (↑z.re + ↑y * Complex.I)) : rectangleIntegral f z w = rectangleIntegral g z w

noncomputable def NumberField.Odlyzko.normalizedRectangleIntegral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (z w : ℂ) : E

A normalized rectangle integral used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.normalizedRectangleIntegral f z w = (1 / (2 * ↑Real.pi * Complex.I)) • NumberField.Odlyzko.rectangleIntegral f z w

def NumberField.Odlyzko.RectangleBorderIntegrable {E : Type u_1} [NormedAddCommGroup E] (f : ℂ → E) (z w : ℂ) : Prop

A rectangle border integrable used in the Odlyzko-bound argument.

Equations

• One or more equations did not get rendered due to their size.

theorem NumberField.Odlyzko.RectangleBorderIntegrable.add_integrable {E : Type u_1} [NormedAddCommGroup E] {f g : ℂ → E} {z w : ℂ} (hf : RectangleBorderIntegrable f z w) (hg : RectangleBorderIntegrable g z w) : RectangleBorderIntegrable (fun (s : ℂ) => f s + g s) z w

theorem NumberField.Odlyzko.rectangleBorderIntegrable_fun_sum {E : Type u_1} [NormedAddCommGroup E] {ι : Type u_2} {T : Finset ι} {f : ι → ℂ → E} {z w : ℂ} (hf : ∀ i ∈ T, RectangleBorderIntegrable (f i) z w) : RectangleBorderIntegrable (fun (s : ℂ) => ∑ i ∈ T, f i s) z w

theorem NumberField.Odlyzko.RectangleBorderIntegrable.add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f g : ℂ → E} {z w : ℂ} (hf : RectangleBorderIntegrable f z w) (hg : RectangleBorderIntegrable g z w) : rectangleIntegral (fun (s : ℂ) => f s + g s) z w = rectangleIntegral f z w + rectangleIntegral g z w

theorem NumberField.Odlyzko.RectangleBorderIntegrable.sub {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f g : ℂ → E} {z w : ℂ} (hf : RectangleBorderIntegrable f z w) (hg : RectangleBorderIntegrable g z w) : rectangleIntegral (fun (s : ℂ) => f s - g s) z w = rectangleIntegral f z w - rectangleIntegral g z w

theorem NumberField.Odlyzko.rectangleIntegral_fun_sum {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {ι : Type u_2} {T : Finset ι} {f : ι → ℂ → E} {z w : ℂ} (hf : ∀ i ∈ T, RectangleBorderIntegrable (f i) z w) : rectangleIntegral (fun (s : ℂ) => ∑ i ∈ T, f i s) z w = ∑ i ∈ T, rectangleIntegral (f i) z w

theorem NumberField.Odlyzko.rectangleIntegral_translate {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (z w p : ℂ) : rectangleIntegral (fun (s : ℂ) => f (s - p)) z w = rectangleIntegral f (z - p) (w - p)

theorem NumberField.Odlyzko.normalizedRectangleIntegral_translate {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (z w p : ℂ) : normalizedRectangleIntegral (fun (s : ℂ) => f (s - p)) z w = normalizedRectangleIntegral f (z - p) (w - p)

theorem NumberField.Odlyzko.rectangleIntegral_const_div_id {z w c : ℂ} (hzre : z.re < 0) (hzim : z.im < 0) (hwre : 0 < w.re) (hwim : 0 < w.im) : rectangleIntegral (fun (s : ℂ) => c / s) z w = 2 * Complex.I * ↑Real.pi * c

theorem NumberField.Odlyzko.normalizedRectangleIntegral_principal {z w p c : ℂ} (hzpre : z.re < p.re) (hprew : p.re < w.re) (hzpim : z.im < p.im) (hpimw : p.im < w.im) : normalizedRectangleIntegral (fun (s : ℂ) => c / (s - p)) z w = c

theorem NumberField.Odlyzko.rectangleIntegral_principal {z w p c : ℂ} (hzpre : z.re < p.re) (hprew : p.re < w.re) (hzpim : z.im < p.im) (hpimw : p.im < w.im) : rectangleIntegral (fun (s : ℂ) => c / (s - p)) z w = 2 * ↑Real.pi * Complex.I * c