PrimeNumberTheoremAnd.ResidueCalcOnRectangles

source

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

Equations

HIntegral f x₁ x₂ y = ∫ (x : ℝ) in x₁..x₂, f (↑x + ↑y * Complex.I)

Instances For

source

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

Equations

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

Instances For

source

noncomputable def HIntegral' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (x₁ x₂ y : ℝ) :

Equations

HIntegral' f x₁ x₂ y = (1 / (2 * ↑Real.pi * Complex.I)) • HIntegral f x₁ x₂ y

Instances For

source

noncomputable def VIntegral' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (x y₁ y₂ : ℝ) :

Equations

VIntegral' f x y₁ y₂ = (1 / (2 * ↑Real.pi * Complex.I)) • VIntegral f x y₁ y₂

Instances For

source

theorem HIntegral_symm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {x₁ x₂ y : ℝ} :

HIntegral f x₁ x₂ y = -HIntegral f x₂ x₁ y

source

theorem VIntegral_symm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {x y₁ y₂ : ℝ} :

VIntegral f x y₁ y₂ = -VIntegral f x y₂ y₁

source

noncomputable def RectangleIntegral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (z w : ℂ) :

A RectangleIntegral of a function f is one over a rectangle determined by z and w in ℂ.

Equations

RectangleIntegral f z w = HIntegral f z.re w.re z.im - HIntegral f z.re w.re w.im + VIntegral f w.re z.im w.im - VIntegral f z.re z.im w.im

Instances For

source

@[reducible, inline]

noncomputable abbrev RectangleIntegral' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (z w : ℂ) :

A RectangleIntegral' of a function f is one over a rectangle determined by z and w in ℂ, divided by 2 * π * I.

Equations

RectangleIntegral' f z w = (1 / (2 * ↑Real.pi * Complex.I)) • RectangleIntegral f z w

Instances For

source

noncomputable def UpperUIntegral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (σ σ' T : ℝ) :

Equations

UpperUIntegral f σ σ' T = (HIntegral f σ σ' T + Complex.I • ∫ (y : ℝ) in Set.Ici T, f (↑σ' + ↑y * Complex.I)) - Complex.I • ∫ (y : ℝ) in Set.Ici T, f (↑σ + ↑y * Complex.I)

Instances For

source

noncomputable def LowerUIntegral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (σ σ' T : ℝ) :

Equations

LowerUIntegral f σ σ' T = (HIntegral f σ σ' (-T) - Complex.I • ∫ (y : ℝ) in Set.Iic (-T), f (↑σ' + ↑y * Complex.I)) + Complex.I • ∫ (y : ℝ) in Set.Iic (-T), f (↑σ + ↑y * Complex.I)

Instances For

source

noncomputable def VerticalIntegral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (σ : ℝ) :

Equations

VerticalIntegral f σ = Complex.I • ∫ (t : ℝ), f (↑σ + ↑t * Complex.I)

Instances For

source

@[reducible, inline]

noncomputable abbrev VerticalIntegral' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (σ : ℝ) :

Equations

VerticalIntegral' f σ = (1 / (2 * ↑Real.pi * Complex.I)) • VerticalIntegral f σ

Instances For

source

theorem verticalIntegral_split_three {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {σ : ℝ} (a b : ℝ) (hf : MeasureTheory.Integrable (fun (t : ℝ) => f (↑σ + ↑t * Complex.I)) MeasureTheory.volume) :

VerticalIntegral f σ = (Complex.I • ∫ (t : ℝ) in Set.Iic a, f (↑σ + ↑t * Complex.I)) + VIntegral f σ a b + Complex.I • ∫ (t : ℝ) in Set.Ici b, f (↑σ + ↑t * Complex.I)

source

theorem DiffVertRect_eq_UpperLowerUs {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {σ σ' T : ℝ} (f_int_σ : MeasureTheory.Integrable (fun (t : ℝ) => f (↑σ + ↑t * Complex.I)) MeasureTheory.volume) (f_int_σ' : MeasureTheory.Integrable (fun (t : ℝ) => f (↑σ' + ↑t * Complex.I)) MeasureTheory.volume) :

VerticalIntegral f σ' - VerticalIntegral f σ - RectangleIntegral f (↑σ - Complex.I * ↑T) (↑σ' + Complex.I * ↑T) = UpperUIntegral f σ σ' T - LowerUIntegral f σ σ' T

source

@[reducible, inline]

abbrev HolomorphicOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (s : Set ℂ) :

Prop

A function is HolomorphicOn a set if it is complex differentiable on that set.

Equations

HolomorphicOn f s = DifferentiableOn ℂ f s

Instances For

source

theorem existsDifferentiableOn_of_bddAbove {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} [CompleteSpace E] {s : Set ℂ} {c : ℂ} (hc : s ∈ nhds c) (hd : HolomorphicOn f (s \ {c})) (hb : BddAbove (norm ∘ f '' (s \ {c}))) :

∃ (g : ℂ → E), HolomorphicOn g s ∧ Set.EqOn f g (s \ {c})

source

theorem HolomorphicOn.vanishesOnRectangle {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {z w : ℂ} [CompleteSpace E] {U : Set ℂ} (f_holo : HolomorphicOn f U) (hU : z.Rectangle w ⊆ U) :

RectangleIntegral f z w = 0

source

theorem RectangleIntegral_congr {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f g : ℂ → E} {z w : ℂ} (h : Set.EqOn f g (RectangleBorder z w)) :

RectangleIntegral f z w = RectangleIntegral g z w

source

theorem RectangleIntegral'_congr {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f g : ℂ → E} {z w : ℂ} (h : Set.EqOn f g (RectangleBorder z w)) :

RectangleIntegral' f z w = RectangleIntegral' g z w

source

theorem rectangleIntegral_symm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (z w : ℂ) :

RectangleIntegral f z w = RectangleIntegral f w z

source

theorem rectangleIntegral_symm_re {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (z w : ℂ) :

RectangleIntegral f (↑w.re + ↑z.im * Complex.I) (↑z.re + ↑w.im * Complex.I) = -RectangleIntegral f z w

source

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

Prop

Equations

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

Instances For

source

theorem RectangleBorderIntegrable.add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {z w : ℂ} {f g : ℂ → E} (hf : RectangleBorderIntegrable f z w) (hg : RectangleBorderIntegrable g z w) :

RectangleIntegral (f + g) z w = RectangleIntegral f z w + RectangleIntegral g z w

source

theorem ContinuousOn.rectangleBorder_integrable {E : Type u_1} [NormedAddCommGroup E] {f : ℂ → E} {z w : ℂ} (hf : ContinuousOn f (RectangleBorder z w)) :

RectangleBorderIntegrable f z w

source

theorem ContinuousOn.rectangleBorderIntegrable {E : Type u_1} [NormedAddCommGroup E] {f : ℂ → E} {z w : ℂ} (hf : ContinuousOn f (z.Rectangle w)) :

RectangleBorderIntegrable f z w

source

theorem ContinuousOn.rectangleBorderNoPIntegrable {E : Type u_1} [NormedAddCommGroup E] {f : ℂ → E} {z w p : ℂ} (hf : ContinuousOn f (z.Rectangle w \ {p})) (pNotOnBorder : p ∉ RectangleBorder z w) :

RectangleBorderIntegrable f z w

source

theorem HolomorphicOn.rectangleBorderIntegrable' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {z w p : ℂ} (hf : HolomorphicOn f (z.Rectangle w \ {p})) (hp : z.Rectangle w ∈ nhds p) :

RectangleBorderIntegrable f z w

source

theorem HolomorphicOn.rectangleBorderIntegrable {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {z w : ℂ} (hf : HolomorphicOn f (z.Rectangle w)) :

RectangleBorderIntegrable f z w

source

theorem RectangleIntegralHSplit {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {a x₀ x₁ y₀ y₁ : ℝ} (f_int_x₀_a_bot : IntervalIntegrable (fun (x : ℝ) => f (↑x + ↑y₀ * Complex.I)) MeasureTheory.volume x₀ a) (f_int_a_x₁_bot : IntervalIntegrable (fun (x : ℝ) => f (↑x + ↑y₀ * Complex.I)) MeasureTheory.volume a x₁) (f_int_x₀_a_top : IntervalIntegrable (fun (x : ℝ) => f (↑x + ↑y₁ * Complex.I)) MeasureTheory.volume x₀ a) (f_int_a_x₁_top : IntervalIntegrable (fun (x : ℝ) => f (↑x + ↑y₁ * Complex.I)) MeasureTheory.volume a x₁) :

RectangleIntegral f (↑x₀ + ↑y₀ * Complex.I) (↑x₁ + ↑y₁ * Complex.I) = RectangleIntegral f (↑x₀ + ↑y₀ * Complex.I) (↑a + ↑y₁ * Complex.I) + RectangleIntegral f (↑a + ↑y₀ * Complex.I) (↑x₁ + ↑y₁ * Complex.I)

Given x₀ a x₁ : ℝ, and y₀ y₁ : ℝ and a function f : ℂ → ℂ so that both (t : ℝ) ↦ f(t + y₀ * I) and (t : ℝ) ↦ f(t + y₁ * I) are integrable over both t ∈ Icc x₀ a and t ∈ Icc a x₁, we have that RectangleIntegral f (x₀ + y₀ * I) (x₁ + y₁ * I) is the sum of RectangleIntegral f (x₀ + y₀ * I) (a + y₁ * I) and RectangleIntegral f (a + y₀ * I) (x₁ + y₁ * I).

source

theorem RectangleIntegralHSplit' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {a x₀ x₁ y₀ y₁ : ℝ} (ha : a ∈ Set.uIcc x₀ x₁) (hf : RectangleBorderIntegrable f (↑x₀ + ↑y₀ * Complex.I) (↑x₁ + ↑y₁ * Complex.I)) :

source

theorem RectangleIntegralVSplit {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {b x₀ x₁ y₀ y₁ : ℝ} (f_int_y₀_b_left : IntervalIntegrable (fun (y : ℝ) => f (↑x₀ + ↑y * Complex.I)) MeasureTheory.volume y₀ b) (f_int_b_y₁_left : IntervalIntegrable (fun (y : ℝ) => f (↑x₀ + ↑y * Complex.I)) MeasureTheory.volume b y₁) (f_int_y₀_b_right : IntervalIntegrable (fun (y : ℝ) => f (↑x₁ + ↑y * Complex.I)) MeasureTheory.volume y₀ b) (f_int_b_y₁_right : IntervalIntegrable (fun (y : ℝ) => f (↑x₁ + ↑y * Complex.I)) MeasureTheory.volume b y₁) :

RectangleIntegral f (↑x₀ + ↑y₀ * Complex.I) (↑x₁ + ↑y₁ * Complex.I) = RectangleIntegral f (↑x₀ + ↑y₀ * Complex.I) (↑x₁ + ↑b * Complex.I) + RectangleIntegral f (↑x₀ + ↑b * Complex.I) (↑x₁ + ↑y₁ * Complex.I)

source

theorem RectangleIntegralVSplit' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {b x₀ x₁ y₀ y₁ : ℝ} (hb : b ∈ Set.uIcc y₀ y₁) (hf : RectangleBorderIntegrable f (↑x₀ + ↑y₀ * Complex.I) (↑x₁ + ↑y₁ * Complex.I)) :

source

theorem RectanglePullToNhdOfPole' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} [CompleteSpace E] {z₀ z₁ z₂ z₃ p : ℂ} (h_orientation : z₀.re ≤ z₃.re ∧ z₀.im ≤ z₃.im ∧ z₁.re ≤ z₂.re ∧ z₁.im ≤ z₂.im) (hp : z₁.Rectangle z₂ ∈ nhds p) (hz : z₁.Rectangle z₂ ⊆ z₀.Rectangle z₃) (fHolo : HolomorphicOn f (z₀.Rectangle z₃ \ {p})) :

RectangleIntegral f z₀ z₃ = RectangleIntegral f z₁ z₂

source

theorem RectanglePullToNhdOfPole {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} [CompleteSpace E] {z w p : ℂ} (zRe_lt_wRe : z.re ≤ w.re) (zIm_lt_wIm : z.im ≤ w.im) (hp : z.Rectangle w ∈ nhds p) (fHolo : HolomorphicOn f (z.Rectangle w \ {p})) :

∀ᶠ (c : ℝ) in nhdsWithin 0 (Set.Ioi 0), RectangleIntegral f z w = RectangleIntegral f (-↑c - Complex.I * ↑c + p) (↑c + Complex.I * ↑c + p)

Given f holomorphic on a rectangle z and w except at a point p, the integral of f over the rectangle with corners z and w is the same as the integral of f over a small square centered at p.

source

theorem RectanglePullToNhdOfPole'' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} [CompleteSpace E] {z w p : ℂ} (zRe_le_wRe : z.re ≤ w.re) (zIm_le_wIm : z.im ≤ w.im) (pInRectInterior : z.Rectangle w ∈ nhds p) (fHolo : HolomorphicOn f (z.Rectangle w \ {p})) :

∀ᶠ (c : ℝ) in nhdsWithin 0 (Set.Ioi 0), RectangleIntegral' f z w = RectangleIntegral' f (-↑c - Complex.I * ↑c + p) (↑c + Complex.I * ↑c + p)

source

theorem ResidueTheoremAtOrigin_aux1c (a b : ℝ) :

let f := fun (y : ℝ) => (↑y + Complex.I)⁻¹; IntervalIntegrable f MeasureTheory.volume a b

source

theorem ResidueTheoremAtOrigin_aux1c' (a b : ℝ) :

let f := fun (y : ℝ) => (↑y - Complex.I)⁻¹; IntervalIntegrable f MeasureTheory.volume a b

source

theorem ResidueTheoremAtOrigin_aux2c (a b : ℝ) :

let f := fun (y : ℝ) => (1 + ↑y * Complex.I)⁻¹; IntervalIntegrable f MeasureTheory.volume a b

source

theorem ResidueTheoremAtOrigin_aux2c' (a b : ℝ) :

let f := fun (y : ℝ) => (-1 + ↑y * Complex.I)⁻¹; IntervalIntegrable f MeasureTheory.volume a b

source

theorem RectangleIntegral.const_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (z w c : ℂ) :

RectangleIntegral (fun (s : ℂ) => c • f s) z w = c • RectangleIntegral f z w

source

theorem RectangleIntegral.const_mul' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (z w c : ℂ) :

RectangleIntegral' (fun (s : ℂ) => c • f s) z w = c • RectangleIntegral' f z w

source

theorem 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)

source

theorem 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)

source

theorem Complex.inv_re_add_im {x y : ℝ} :

(↑x + ↑y * I)⁻¹ = (↑x - I * ↑y) / (↑x ^ 2 + ↑y ^ 2)

source

theorem sq_add_sq_ne_zero {x y : ℝ} (hy : y ≠ 0) :

x ^ 2 + y ^ 2 ≠ 0

source

theorem continuous_self_div_sq_add_sq {y : ℝ} (hy : y ≠ 0) :

Continuous fun (x : ℝ) => x / (x ^ 2 + y ^ 2)

source

theorem integral_self_div_sq_add_sq {x₁ x₂ y : ℝ} (hy : y ≠ 0) :

∫ (x : ℝ) in x₁..x₂, x / (x ^ 2 + y ^ 2) = Real.log (x₂ ^ 2 + y ^ 2) / 2 - Real.log (x₁ ^ 2 + y ^ 2) / 2

source

theorem integral_const_div_sq_add_sq {x₁ x₂ y : ℝ} (hy : y ≠ 0) :

∫ (x : ℝ) in x₁..x₂, y / (x ^ 2 + y ^ 2) = Real.arctan (x₂ / y) - Real.arctan (x₁ / y)

source

theorem integral_const_div_self_add_im {A : ℂ} {x₁ x₂ y : ℝ} (hy : y ≠ 0) :

∫ (x : ℝ) in x₁..x₂, A / (↑x + ↑y * Complex.I) = A * (↑(Real.log (x₂ ^ 2 + y ^ 2)) / 2 - ↑(Real.log (x₁ ^ 2 + y ^ 2)) / 2) - A * Complex.I * (↑(Real.arctan (x₂ / y)) - ↑(Real.arctan (x₁ / y)))

source

theorem integral_const_div_re_add_self {A : ℂ} {x y₁ y₂ : ℝ} (hx : x ≠ 0) :

∫ (y : ℝ) in y₁..y₂, A / (↑x + ↑y * Complex.I) = A / Complex.I * (↑(Real.log (y₂ ^ 2 + (-x) ^ 2)) / 2 - ↑(Real.log (y₁ ^ 2 + (-x) ^ 2)) / 2) - A / Complex.I * Complex.I * (↑(Real.arctan (y₂ / -x)) - ↑(Real.arctan (y₁ / -x)))

source

theorem ResidueTheoremAtOrigin' {z w c : ℂ} (h1 : z.re < 0) (h2 : z.im < 0) (h3 : 0 < w.re) (h4 : 0 < w.im) :

RectangleIntegral (fun (s : ℂ) => c / s) z w = 2 * Complex.I * ↑Real.pi * c

source

theorem ResidueTheoremInRectangle {z w p c : ℂ} (zRe_le_wRe : z.re ≤ w.re) (zIm_le_wIm : z.im ≤ w.im) (pInRectInterior : z.Rectangle w ∈ nhds p) :

RectangleIntegral' (fun (s : ℂ) => c / (s - p)) z w = c

source

theorem ResidueTheoremAtOrigin :

RectangleIntegral' (fun (s : ℂ) => 1 / s) (-1 - Complex.I) (1 + Complex.I) = 1

source

theorem ResidueTheoremOnRectangleWithSimplePole {f g : ℂ → ℂ} {z w p A : ℂ} (zRe_le_wRe : z.re ≤ w.re) (zIm_le_wIm : z.im ≤ w.im) (pInRectInterior : z.Rectangle w ∈ nhds p) (gHolo : HolomorphicOn g (z.Rectangle w)) (principalPart : Set.EqOn (f - fun (s : ℂ) => A / (s - p)) g (z.Rectangle w \ {p})) :

RectangleIntegral' f z w = A