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

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

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

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

State before:
case h
x σ✝ σ'✝ σ'' T✝ : ℝ
f : ℂ → ℂ
σ σ' T : ℝ
hσ : σ ≤ σ'
hf : HolomorphicOn f {z | σ ≤ z.re ∧ z.re ≤ σ' ∧ T ≤ z.im}
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
⊢ ∀ (a : ℝ), T ≤ a → RectangleIntegral f (↑σ + I * ↑T) (↑σ' + I * ↑a) = 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 ≤ σ' ∧ T ≤ z.im}
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 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 * ↑T) (↑σ' + I * ↑x✝¹) → x✝ ∈ {z | σ ≤ z.re ∧ z.re ≤ σ' ∧ T ≤ z.im}

State before:
case h
x σ✝ σ'✝ σ'' T✝ : ℝ
f : ℂ → ℂ
σ σ' T : ℝ
hσ : σ ≤ σ'
hf : HolomorphicOn f {z | σ ≤ z.re ∧ z.re ≤ σ' ∧ T ≤ z.im}
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 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 * ↑T) (↑σ' + I * ↑x✝¹) → x✝ ∈ {z | σ ≤ z.re ∧ z.re ≤ σ' ∧ T ≤ z.im}
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 ≤ σ' ∧ T ≤ z.im}
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
x✝¹ : ℝ
hTU : T ≤ x✝¹
x✝ : ℂ
⊢ (↑σ + I * ↑T).re ≤ x✝.re ∧ x✝.re ≤ (↑σ' + I * ↑x✝¹).re ∧ (↑σ + I * ↑T).im ≤ x✝.im ∧ x✝.im ≤ (↑σ' + I * ↑x✝¹).im →
    x✝ ∈ {z | σ ≤ z.re ∧ z.re ≤ σ' ∧ T ≤ z.im}

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

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

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

State before:
x σ✝ σ'✝ σ'' T✝ : ℝ
f : ℂ → ℂ
σ σ' T : ℝ
hσ : σ ≤ σ'
hf : HolomorphicOn f {z | σ ≤ z.re ∧ z.re ≤ σ' ∧ T ≤ z.im}
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 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 ≤ σ' → T ≤ x✝.im → x✝.im ≤ x✝¹ → σ ≤ x✝.re ∧ x✝.re ≤ σ' ∧ T ≤ x✝.im
Tactic:
tauto
State after:
no goals