Theorem: verticalIntegral_eq_verticalIntegral (PrimeNumberTheoremAnd/PerronFormula.lean)

State before:
σ σ' : ℝ
f : ℂ → ℂ
hf : HolomorphicOn f ([[σ, σ']] ×ℂ univ)
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
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
⊢ VerticalIntegral f σ = VerticalIntegral f σ'
Tactic:
refine zeroTendstoDiff _ _ _ (univ_mem' fun _ ↦ ?_)
  (RectangleIntegral_tendsTo_VerticalIntegral hbot htop hleft hright)
State after:
σ σ' : ℝ
f : ℂ → ℂ
hf : HolomorphicOn f ([[σ, σ']] ×ℂ univ)
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
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✝ : ℝ
⊢ x✝ ∈ {x | (fun T => RectangleIntegral f (↑σ - I * ↑T) (↑σ' + I * ↑T) = 0) x}

State before:
σ σ' : ℝ
f : ℂ → ℂ
hf : HolomorphicOn f ([[σ, σ']] ×ℂ univ)
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
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✝ : ℝ
⊢ x✝ ∈ {x | (fun T => RectangleIntegral f (↑σ - I * ↑T) (↑σ' + I * ↑T) = 0) x}
Tactic:
exact integral_boundary_rect_eq_zero_of_differentiableOn f _ _
  (hf.mono fun z hrect ↦ ⟨by simpa using hrect.1, trivial⟩)
State after:
no goals

State before:
σ σ' : ℝ
f : ℂ → ℂ
hf : HolomorphicOn f ([[σ, σ']] ×ℂ univ)
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
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✝ : ℝ
z : ℂ
hrect : z ∈ [[(↑σ - I * ↑x✝).re, (↑σ' + I * ↑x✝).re]] ×ℂ [[(↑σ - I * ↑x✝).im, (↑σ' + I * ↑x✝).im]]
⊢ z ∈ re ⁻¹' [[σ, σ']]
Tactic:
simpa using hrect.1
State after:
no goals