theorem zeroTendstoDiff (L₁ L₂ : ℂ) (f : ℝ → ℂ) (h : ∀ᶠ (T : ℝ) in Filter.atTop, f T = 0) (h' : Filter.Tendsto f Filter.atTop (nhds (L₂ - L₁))) : L₁ = L₂

theorem RectangleIntegral_tendsTo_VerticalIntegral {σ σ' : ℝ} {f : ℂ → ℂ} (hbot : Filter.Tendsto (fun (y : ℝ) => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * Complex.I)) Filter.atBot (nhds 0)) (htop : Filter.Tendsto (fun (y : ℝ) => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * Complex.I)) Filter.atTop (nhds 0)) (hleft : MeasureTheory.Integrable (fun (y : ℝ) => f (↑σ + ↑y * Complex.I)) MeasureTheory.volume) (hright : MeasureTheory.Integrable (fun (y : ℝ) => f (↑σ' + ↑y * Complex.I)) MeasureTheory.volume) : Filter.Tendsto (fun (T : ℝ) => RectangleIntegral f (↑σ - Complex.I * ↑T) (↑σ' + Complex.I * ↑T)) Filter.atTop (nhds (VerticalIntegral f σ' - VerticalIntegral f σ))

theorem verticalIntegral_eq_verticalIntegral {σ σ' : ℝ} {f : ℂ → ℂ} (hf : HolomorphicOn f (Set.uIcc σ σ' ×ℂ Set.univ)) (hbot : Filter.Tendsto (fun (y : ℝ) => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * Complex.I)) Filter.atBot (nhds 0)) (htop : Filter.Tendsto (fun (y : ℝ) => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * Complex.I)) Filter.atTop (nhds 0)) (hleft : MeasureTheory.Integrable (fun (y : ℝ) => f (↑σ + ↑y * Complex.I)) MeasureTheory.volume) (hright : MeasureTheory.Integrable (fun (y : ℝ) => f (↑σ' + ↑y * Complex.I)) MeasureTheory.volume) : VerticalIntegral f σ = VerticalIntegral f σ'

theorem verticalIntegral_sub_verticalIntegral_eq_squareIntegral {σ σ' : ℝ} {f : ℂ → ℂ} {p : ℂ} (hσ : σ < p.re ∧ p.re < σ') (hf : HolomorphicOn f (Set.Icc σ σ' ×ℂ Set.univ \ {p})) (hbot : Filter.Tendsto (fun (y : ℝ) => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * Complex.I)) Filter.atBot (nhds 0)) (htop : Filter.Tendsto (fun (y : ℝ) => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * Complex.I)) Filter.atTop (nhds 0)) (hleft : MeasureTheory.Integrable (fun (y : ℝ) => f (↑σ + ↑y * Complex.I)) MeasureTheory.volume) (hright : MeasureTheory.Integrable (fun (y : ℝ) => f (↑σ' + ↑y * Complex.I)) MeasureTheory.volume) : ∀ᶠ (c : ℝ) in nhdsWithin 0 (Set.Ioi 0), VerticalIntegral f σ' - VerticalIntegral f σ = RectangleIntegral f (-↑c - ↑c * Complex.I + p) (↑c + ↑c * Complex.I + p)

theorem RectangleIntegral_tendsTo_UpperU {σ σ' T : ℝ} {f : ℂ → ℂ} (htop : Filter.Tendsto (fun (y : ℝ) => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * Complex.I)) Filter.atTop (nhds 0)) (hleft : MeasureTheory.Integrable (fun (y : ℝ) => f (↑σ + ↑y * Complex.I)) MeasureTheory.volume) (hright : MeasureTheory.Integrable (fun (y : ℝ) => f (↑σ' + ↑y * Complex.I)) MeasureTheory.volume) : Filter.Tendsto (fun (U : ℝ) => RectangleIntegral f (↑σ + Complex.I * ↑T) (↑σ' + Complex.I * ↑U)) Filter.atTop (nhds (UpperUIntegral f σ σ' T))

theorem RectangleIntegral_tendsTo_LowerU {σ σ' T : ℝ} {f : ℂ → ℂ} (hbot : Filter.Tendsto (fun (y : ℝ) => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * Complex.I)) Filter.atBot (nhds 0)) (hleft : MeasureTheory.Integrable (fun (y : ℝ) => f (↑σ + ↑y * Complex.I)) MeasureTheory.volume) (hright : MeasureTheory.Integrable (fun (y : ℝ) => f (↑σ' + ↑y * Complex.I)) MeasureTheory.volume) : Filter.Tendsto (fun (U : ℝ) => RectangleIntegral f (↑σ - Complex.I * ↑U) (↑σ' - Complex.I * ↑T)) Filter.atTop (nhds (-LowerUIntegral f σ σ' T))

theorem limitOfConstant {a : ℝ → ℂ} {σ : ℝ} (σpos : 0 < σ) (ha : ∀ (σ' σ'' : ℝ), 0 < σ' → 0 < σ'' → a σ' = a σ'') (ha' : Filter.Tendsto a Filter.atTop (nhds 0)) : a σ = 0

theorem limitOfConstantLeft {a : ℝ → ℂ} {σ : ℝ} (σlt : σ ≤ -3 / 2) (ha : ∀ (σ' σ'' : ℝ), σ' ≤ -3 / 2 → σ'' ≤ -3 / 2 → a σ' = a σ'') (ha' : Filter.Tendsto a Filter.atBot (nhds 0)) : a σ = 0

theorem tendsto_rpow_atTop_nhds_zero_of_norm_lt_one {x : ℝ} (xpos : 0 < x) (x_lt_one : x < 1) (C : ℝ) : Filter.Tendsto (fun (σ : ℝ) => x ^ σ * C) Filter.atTop (nhds 0)

theorem tendsto_rpow_atTop_nhds_zero_of_norm_gt_one {x : ℝ} (x_gt_one : 1 < x) (C : ℝ) : Filter.Tendsto (fun (σ : ℝ) => x ^ σ * C) Filter.atBot (nhds 0)

theorem Complex.cpow_eq_exp_log_ofReal (x : ℝ) (hx : 0 < x) (y : ℂ) : ↑x ^ y = exp (↑(Real.log x) * y)

theorem Complex.cpow_neg_eq_inv_pow_ofReal_pos {a : ℝ} (ha : 0 < a) (r : ℂ) : ↑a ^ (-r) = (↑a)⁻¹ ^ r

@[reducible, inline]

noncomputable abbrev Perron.f (x : ℝ) (s : ℂ) : ℂ

Equations

• Perron.f x s = ↑x ^ s / (s * (s + 1))

theorem Perron.f_mul_eq_f {x t : ℝ} (tpos : 0 < t) (xpos : 0 < x) (s : ℂ) : f t s * ↑x ^ (-s) = f (t / x) s

theorem Perron.isHolomorphicOn {x : ℝ} (xpos : 0 < x) : HolomorphicOn (f x) {0, -1}ᶜ

theorem Perron.integral_one_div_const_add_sq_pos (c : ℝ) (hc : 0 < c) : 0 < ∫ (t : ℝ), 1 / (c + t ^ 2)

theorem Perron.Integrable.one_div_const_add_sq (c : ℝ) (hc : 0 < c) : MeasureTheory.Integrable (fun (t : ℝ) => 1 / (c + t ^ 2)) MeasureTheory.volume

theorem Perron.integralPosAux'_of_le (c₁ c₂ : ℝ) (c₁_pos : 0 < c₁) (hle : c₁ ≤ c₂) : 0 < ∫ (t : ℝ), 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2))

theorem Perron.integralPosAux' (c₁ c₂ : ℝ) (c₁_pos : 0 < c₁) (c₂_pos : 0 < c₂) : 0 < ∫ (t : ℝ), 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2))

theorem Perron.integralPosAux : 0 < ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2))

theorem Perron.vertIntBound {x σ : ℝ} (xpos : 0 < x) (σ_gt_one : 1 < σ) : ‖VerticalIntegral (f x) σ‖ ≤ x ^ σ * ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2))

theorem Perron.vertIntBoundLeft {x : ℝ} (xpos : 0 < x) : ∃ (C : ℝ), ∀ σ < -3 / 2, ‖VerticalIntegral' (f x) σ‖ ≤ C * x ^ σ

theorem Perron.map_conj {x : ℝ} (hx : 0 ≤ x) (s : ℂ) : f x ((starRingEnd ℂ) s) = (starRingEnd ℂ) (f x s)

theorem Perron.isTheta_uniformlyOn_uIcc {x : ℝ} (xpos : 0 < x) (σ' σ'' : ℝ) : (fun (x_1 : ℝ × ℝ) => match x_1 with | (σ, y) => f x (↑σ + ↑y * Complex.I)) =Θ[Filter.principal (Set.uIcc σ' σ'') ×ˢ (Filter.atBot ⊔ Filter.atTop)] ((fun (y : ℝ) => 1 / y ^ 2) ∘ Prod.snd)

theorem Perron.isTheta_uniformlyOn_uIoc {x : ℝ} (xpos : 0 < x) (σ' σ'' : ℝ) : (fun (x_1 : ℝ × ℝ) => match x_1 with | (σ, y) => f x (↑σ + ↑y * Complex.I)) =Θ[Filter.principal (Set.uIoc σ' σ'') ×ˢ (Filter.atBot ⊔ Filter.atTop)] fun (x : ℝ × ℝ) => match x with | (fst, y) => 1 / y ^ 2

theorem Perron.isTheta {x σ : ℝ} (xpos : 0 < x) : ((fun (y : ℝ) => f x (↑σ + ↑y * Complex.I)) =Θ[Filter.atBot] fun (y : ℝ) => 1 / y ^ 2) ∧ (fun (y : ℝ) => f x (↑σ + ↑y * Complex.I)) =Θ[Filter.atTop] fun (y : ℝ) => 1 / y ^ 2

theorem Perron.isIntegrable {x σ : ℝ} (xpos : 0 < x) (σ_ne_zero : σ ≠ 0) (σ_ne_neg_one : σ ≠ -1) : MeasureTheory.Integrable (fun (t : ℝ) => f x (↑σ + ↑t * Complex.I)) MeasureTheory.volume

theorem Perron.horizontal_integral_isBigO {x : ℝ} (xpos : 0 < x) (σ' σ'' : ℝ) (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsLocallyFiniteMeasure μ] : (fun (y : ℝ) => ∫ (σ : ℝ) in σ'..σ'', f x (↑σ + ↑y * Complex.I) ∂μ) =O[Filter.atBot ⊔ Filter.atTop] fun (y : ℝ) => 1 / y ^ 2

theorem Perron.tendsto_zero_Lower {x : ℝ} (xpos : 0 < x) (σ' σ'' : ℝ) : Filter.Tendsto (fun (t : ℝ) => ∫ (σ : ℝ) in σ'..σ'', f x (↑σ + ↑t * Complex.I)) Filter.atBot (nhds 0)

theorem Perron.tendsto_zero_Upper {x : ℝ} (xpos : 0 < x) (σ' σ'' : ℝ) : Filter.Tendsto (fun (t : ℝ) => ∫ (σ : ℝ) in σ'..σ'', f x (↑σ + ↑t * Complex.I)) Filter.atTop (nhds 0)

theorem Perron.contourPull {x σ' σ'' : ℝ} (xpos : 0 < x) (hσ0 : 0 ∉ Set.uIcc σ' σ'') (hσ1 : -1 ∉ Set.uIcc σ' σ'') : VerticalIntegral (f x) σ' = VerticalIntegral (f x) σ''

theorem Perron.formulaLtOne {x σ : ℝ} (xpos : 0 < x) (x_lt_one : x < 1) (σ_pos : 0 < σ) : VerticalIntegral (f x) σ = 0

theorem Perron.HolomorphicOn.upperUIntegral_eq_zero {f : ℂ → ℂ} {σ σ' T : ℝ} (hσ : σ ≤ σ') (hf : HolomorphicOn f {z : ℂ | σ ≤ z.re ∧ z.re ≤ σ' ∧ T ≤ z.im}) (htop : Filter.Tendsto (fun (y : ℝ) => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * Complex.I)) Filter.atTop (nhds 0)) (hleft : MeasureTheory.Integrable (fun (y : ℝ) => f (↑σ + ↑y * Complex.I)) MeasureTheory.volume) (hright : MeasureTheory.Integrable (fun (y : ℝ) => f (↑σ' + ↑y * Complex.I)) MeasureTheory.volume) : UpperUIntegral f σ σ' T = 0

theorem Perron.HolomorphicOn.lowerUIntegral_eq_zero {f : ℂ → ℂ} {σ σ' T : ℝ} (hσ : σ ≤ σ') (hf : HolomorphicOn f {z : ℂ | σ ≤ z.re ∧ z.re ≤ σ' ∧ z.im ≤ -T}) (hbot : Filter.Tendsto (fun (y : ℝ) => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * Complex.I)) Filter.atBot (nhds 0)) (hleft : MeasureTheory.Integrable (fun (y : ℝ) => f (↑σ + ↑y * Complex.I)) MeasureTheory.volume) (hright : MeasureTheory.Integrable (fun (y : ℝ) => f (↑σ' + ↑y * Complex.I)) MeasureTheory.volume) : LowerUIntegral f σ σ' T = 0

theorem Perron.sPlusOneNeZero {s : ℂ} (s_ne_neg_one : s ≠ -1) : s + 1 ≠ 0

theorem Perron.keyIdentity (x : ℝ) {s : ℂ} (s_ne_zero : s ≠ 0) (s_ne_neg_one : s ≠ -1) : ↑x ^ s / (s * (s + 1)) = ↑x ^ s / s - ↑x ^ s / (s + 1)

theorem Filter.Tendsto.eventually_bddAbove {α : Type u_1} {β : Type u_2} [LinearOrder β] [NoMaxOrder β] [TopologicalSpace β] [ClosedIciTopology β] {y : β} {l : Filter α} {f : α → β} (hf : Tendsto f l (nhds y)) : ∀ᶠ (s : Set α) in l.smallSets, BddAbove (f '' s)

theorem Perron.bddAbove_square_of_tendsto {β : Type u_2} [LinearOrder β] [NoMaxOrder β] [TopologicalSpace β] [ClosedIciTopology β] {y : β} {f : ℂ → β} {x : ℂ} (hf : Filter.Tendsto f (nhdsWithin x {x}ᶜ) (nhds y)) : ∀ᶠ (c : ℝ) in nhdsWithin 0 (Set.Ioi 0), BddAbove (f '' (Square x c \ {x}))

theorem Perron.diffBddAtZero {x : ℝ} (xpos : 0 < x) : ∀ᶠ (c : ℝ) in nhdsWithin 0 (Set.Ioi 0), BddAbove ((norm ∘ fun (s : ℂ) => ↑x ^ s / (s * (s + 1)) - 1 / s) '' (Square 0 c \ {0}))

theorem Perron.diffBddAtNegOne {x : ℝ} (xpos : 0 < x) : ∀ᶠ (c : ℝ) in nhdsWithin 0 (Set.Ioi 0), BddAbove ((norm ∘ fun (s : ℂ) => ↑x ^ s / (s * (s + 1)) - -↑x⁻¹ / (s + 1)) '' (Square (-1) c \ {-1}))

theorem Perron.residueAtZero {x : ℝ} (xpos : 0 < x) : ∀ᶠ (c : ℝ) in nhdsWithin 0 (Set.Ioi 0), RectangleIntegral' (f x) (-↑c - ↑c * Complex.I) (↑c + ↑c * Complex.I) = 1

theorem Perron.residueAtNegOne {x : ℝ} (xpos : 0 < x) : ∀ᶠ (c : ℝ) in nhdsWithin 0 (Set.Ioi 0), RectangleIntegral' (f x) (-↑c - ↑c * Complex.I - 1) (↑c + ↑c * Complex.I - 1) = -↑x⁻¹

theorem Perron.residuePull1 {x σ : ℝ} (x_gt_one : 1 < x) (σ_pos : 0 < σ) : VerticalIntegral' (f x) σ = 1 + VerticalIntegral' (f x) (-1 / 2)

theorem Perron.residuePull2 {x : ℝ} (x_gt_one : 1 < x) : VerticalIntegral' (fun (s : ℂ) => ↑x ^ s / (s * (s + 1))) (-1 / 2) = -1 / ↑x + VerticalIntegral' (fun (s : ℂ) => ↑x ^ s / (s * (s + 1))) (-3 / 2)

theorem Perron.contourPull3 {x σ' σ'' : ℝ} (x_gt_one : 1 < x) (σ'le : σ' ≤ -3 / 2) (σ''le : σ'' ≤ -3 / 2) : VerticalIntegral' (fun (s : ℂ) => ↑x ^ s / (s * (s + 1))) σ' = VerticalIntegral' (fun (s : ℂ) => ↑x ^ s / (s * (s + 1))) σ''

theorem Perron.formulaGtOne {x σ : ℝ} (x_gt_one : 1 < x) (σ_pos : 0 < σ) : VerticalIntegral' (fun (s : ℂ) => ↑x ^ s / (s * (s + 1))) σ = 1 - 1 / ↑x