Theorem: Perron.HolomorphicOn.lowerUIntegral_eq_zero (PrimeNumberTheoremAnd/PerronFormula.lean)

State before:
x σ✝ σ'✝ σ'' T✝ : ℝ
f : ℂ → ℂ
σ σ' T : ℝ
hσ : σ ≤ σ'
hf : HolomorphicOn f {z | σ ≤ z.re ∧ z.re ≤ σ' ∧ z.im ≤ -T}
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
⊢ LowerUIntegral f σ σ' T = 0
Tactic:
suffices h : - LowerUIntegral f σ σ' T = 0 by exact neg_eq_zero.mp h
State after:
x σ✝ σ'✝ σ'' T✝ : ℝ
f : ℂ → ℂ
σ σ' T : ℝ
hσ : σ ≤ σ'
hf : HolomorphicOn f {z | σ ≤ z.re ∧ z.re ≤ σ' ∧ z.im ≤ -T}
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
⊢ -LowerUIntegral f σ σ' T = 0

State before:
x σ✝ σ'✝ σ'' T✝ : ℝ
f : ℂ → ℂ
σ σ' T : ℝ
hσ : σ ≤ σ'
hf : HolomorphicOn f {z | σ ≤ z.re ∧ z.re ≤ σ' ∧ z.im ≤ -T}
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
⊢ -LowerUIntegral f σ σ' T = 0
Tactic:
apply tendsto_nhds_unique (RectangleIntegral_tendsTo_LowerU hbot hleft hright)
State after:
x σ✝ σ'✝ σ'' T✝ : ℝ
f : ℂ → ℂ
σ σ' T : ℝ
hσ : σ ≤ σ'
hf : HolomorphicOn f {z | σ ≤ z.re ∧ z.re ≤ σ' ∧ z.im ≤ -T}
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
⊢ Tendsto (fun U => RectangleIntegral f (↑σ - I * ↑U) (↑σ' - I * ↑T)) atTop (𝓝 0)

State before:
x σ✝ σ'✝ σ'' T✝ : ℝ
f : ℂ → ℂ
σ σ' T : ℝ
hσ : σ ≤ σ'
hf : HolomorphicOn f {z | σ ≤ z.re ∧ z.re ≤ σ' ∧ z.im ≤ -T}
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
⊢ Tendsto (fun U => RectangleIntegral f (↑σ - I * ↑U) (↑σ' - I * ↑T)) atTop (𝓝 0)
Tactic:
apply EventuallyEq.tendsto
State after:
case hf
x σ✝ σ'✝ σ'' T✝ : ℝ
f : ℂ → ℂ
σ σ' T : ℝ
hσ : σ ≤ σ'
hf : HolomorphicOn f {z | σ ≤ z.re ∧ z.re ≤ σ' ∧ z.im ≤ -T}
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
⊢ (fun U => RectangleIntegral f (↑σ - I * ↑U) (↑σ' - I * ↑T)) =ᶠ[atTop] fun x => 0

State before:
case hf
x σ✝ σ'✝ σ'' T✝ : ℝ
f : ℂ → ℂ
σ σ' T : ℝ
hσ : σ ≤ σ'
hf : HolomorphicOn f {z | σ ≤ z.re ∧ z.re ≤ σ' ∧ z.im ≤ -T}
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
⊢ (fun U => RectangleIntegral f (↑σ - I * ↑U) (↑σ' - I * ↑T)) =ᶠ[atTop] fun x => 0
Tactic:
filter_upwards [eventually_ge_atTop T]
State after:
case h
x σ✝ σ'✝ σ'' T✝ : ℝ
f : ℂ → ℂ
σ σ' T : ℝ
hσ : σ ≤ σ'
hf : HolomorphicOn f {z | σ ≤ z.re ∧ z.re ≤ σ' ∧ z.im ≤ -T}
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
⊢ ∀ (a : ℝ), T ≤ a → RectangleIntegral f (↑σ - I * ↑a) (↑σ' - I * ↑T) = 0

State before:
case h
x σ✝ σ'✝ σ'' T✝ : ℝ
f : ℂ → ℂ
σ σ' T : ℝ
hσ : σ ≤ σ'
hf : HolomorphicOn f {z | σ ≤ z.re ∧ z.re ≤ σ' ∧ z.im ≤ -T}
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
⊢ ∀ (a : ℝ), T ≤ a → RectangleIntegral f (↑σ - I * ↑a) (↑σ' - I * ↑T) = 0
Tactic:
refine fun _ hTU ↦ hf.vanishesOnRectangle fun _ ↦ ?_
State after:
case h
x σ✝ σ'✝ σ'' T✝ : ℝ
f : ℂ → ℂ
σ σ' T : ℝ
hσ : σ ≤ σ'
hf : HolomorphicOn f {z | σ ≤ z.re ∧ z.re ≤ σ' ∧ z.im ≤ -T}
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
x✝¹ : ℝ
hTU : T ≤ x✝¹
x✝ : ℂ
⊢ x✝ ∈ Rectangle (↑σ - I * ↑x✝¹) (↑σ' - I * ↑T) → x✝ ∈ {z | σ ≤ z.re ∧ z.re ≤ σ' ∧ z.im ≤ -T}

State before:
case h
x σ✝ σ'✝ σ'' T✝ : ℝ
f : ℂ → ℂ
σ σ' T : ℝ
hσ : σ ≤ σ'
hf : HolomorphicOn f {z | σ ≤ z.re ∧ z.re ≤ σ' ∧ z.im ≤ -T}
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
x✝¹ : ℝ
hTU : T ≤ x✝¹
x✝ : ℂ
⊢ x✝ ∈ Rectangle (↑σ - I * ↑x✝¹) (↑σ' - I * ↑T) → x✝ ∈ {z | σ ≤ z.re ∧ z.re ≤ σ' ∧ z.im ≤ -T}
Tactic:
rw [mem_Rect (by simp [hσ]) (by simp [hTU])]
State after:
case h
x σ✝ σ'✝ σ'' T✝ : ℝ
f : ℂ → ℂ
σ σ' T : ℝ
hσ : σ ≤ σ'
hf : HolomorphicOn f {z | σ ≤ z.re ∧ z.re ≤ σ' ∧ z.im ≤ -T}
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
x✝¹ : ℝ
hTU : T ≤ x✝¹
x✝ : ℂ
⊢ (↑σ - I * ↑x✝¹).re ≤ x✝.re ∧ x✝.re ≤ (↑σ' - I * ↑T).re ∧ (↑σ - I * ↑x✝¹).im ≤ x✝.im ∧ x✝.im ≤ (↑σ' - I * ↑T).im →
    x✝ ∈ {z | σ ≤ z.re ∧ z.re ≤ σ' ∧ z.im ≤ -T}

State before:
case h
x σ✝ σ'✝ σ'' T✝ : ℝ
f : ℂ → ℂ
σ σ' T : ℝ
hσ : σ ≤ σ'
hf : HolomorphicOn f {z | σ ≤ z.re ∧ z.re ≤ σ' ∧ z.im ≤ -T}
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
x✝¹ : ℝ
hTU : T ≤ x✝¹
x✝ : ℂ
⊢ (↑σ - I * ↑x✝¹).re ≤ x✝.re ∧ x✝.re ≤ (↑σ' - I * ↑T).re ∧ (↑σ - I * ↑x✝¹).im ≤ x✝.im ∧ x✝.im ≤ (↑σ' - I * ↑T).im →
    x✝ ∈ {z | σ ≤ z.re ∧ z.re ≤ σ' ∧ z.im ≤ -T}
Tactic:
simpa using by tauto
State after:
no goals

State before:
x σ✝ σ'✝ σ'' T✝ : ℝ
f : ℂ → ℂ
σ σ' T : ℝ
hσ : σ ≤ σ'
hf : HolomorphicOn f {z | σ ≤ z.re ∧ z.re ≤ σ' ∧ z.im ≤ -T}
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
h : -LowerUIntegral f σ σ' T = 0
⊢ LowerUIntegral f σ σ' T = 0
Tactic:
exact neg_eq_zero.mp h
State after:
no goals

State before:
x σ✝ σ'✝ σ'' T✝ : ℝ
f : ℂ → ℂ
σ σ' T : ℝ
hσ : σ ≤ σ'
hf : HolomorphicOn f {z | σ ≤ z.re ∧ z.re ≤ σ' ∧ z.im ≤ -T}
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
x✝¹ : ℝ
hTU : T ≤ x✝¹
x✝ : ℂ
⊢ (↑σ - I * ↑x✝¹).re ≤ (↑σ' - I * ↑T).re
Tactic:
simp [hσ]
State after:
no goals

State before:
x σ✝ σ'✝ σ'' T✝ : ℝ
f : ℂ → ℂ
σ σ' T : ℝ
hσ : σ ≤ σ'
hf : HolomorphicOn f {z | σ ≤ z.re ∧ z.re ≤ σ' ∧ z.im ≤ -T}
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
x✝¹ : ℝ
hTU : T ≤ x✝¹
x✝ : ℂ
⊢ (↑σ - I * ↑x✝¹).im ≤ (↑σ' - I * ↑T).im
Tactic:
simp [hTU]
State after:
no goals

State before:
x σ✝ σ'✝ σ'' T✝ : ℝ
f : ℂ → ℂ
σ σ' T : ℝ
hσ : σ ≤ σ'
hf : HolomorphicOn f {z | σ ≤ z.re ∧ z.re ≤ σ' ∧ z.im ≤ -T}
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
x✝¹ : ℝ
hTU : T ≤ x✝¹
x✝ : ℂ
⊢ σ ≤ x✝.re → x✝.re ≤ σ' → -x✝¹ ≤ x✝.im → x✝.im ≤ -T → σ ≤ x✝.re ∧ x✝.re ≤ σ' ∧ x✝.im ≤ -T
Tactic:
tauto
State after:
no goals