Theorem: RectangleIntegral_tendsTo_VerticalIntegral (PrimeNumberTheoremAnd/PerronFormula.lean)

State before:
σ σ' : ℝ
f : ℂ → ℂ
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
⊢ Tendsto (fun T => RectangleIntegral f (↑σ - I * ↑T) (↑σ' + I * ↑T)) atTop
    (𝓝 (VerticalIntegral f σ' - VerticalIntegral f σ))
Tactic:
simp only [RectangleIntegral, sub_re, ofReal_re, mul_re, I_re, zero_mul, I_im, ofReal_im,
  mul_zero, sub_self, sub_zero, add_re, add_zero, sub_im, mul_im, one_mul, zero_add, zero_sub,
  add_im]
State after:
σ σ' : ℝ
f : ℂ → ℂ
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
⊢ Tendsto (fun T => HIntegral f σ σ' (-T) - HIntegral f σ σ' T + VIntegral f σ' (-T) T - VIntegral f σ (-T) T) atTop
    (𝓝 (VerticalIntegral f σ' - VerticalIntegral f σ))

State before:
σ σ' : ℝ
f : ℂ → ℂ
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
⊢ Tendsto (fun T => HIntegral f σ σ' (-T) - HIntegral f σ σ' T + VIntegral f σ' (-T) T - VIntegral f σ (-T) T) atTop
    (𝓝 (VerticalIntegral f σ' - VerticalIntegral f σ))
Tactic:
apply Tendsto.sub
State after:
case hf
σ σ' : ℝ
f : ℂ → ℂ
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
⊢ Tendsto (fun x => HIntegral f σ σ' (-x) - HIntegral f σ σ' x + VIntegral f σ' (-x) x) atTop
    (𝓝 (VerticalIntegral f σ'))

case hg
σ σ' : ℝ
f : ℂ → ℂ
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
⊢ Tendsto (fun x => VIntegral f σ (-x) x) atTop (𝓝 (VerticalIntegral f σ))

State before:
case hf
σ σ' : ℝ
f : ℂ → ℂ
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
⊢ Tendsto (fun x => HIntegral f σ σ' (-x) - HIntegral f σ σ' x + VIntegral f σ' (-x) x) atTop
    (𝓝 (VerticalIntegral f σ'))
Tactic:
rewrite [← zero_add (VerticalIntegral _ _), ← zero_sub_zero]
State after:
case hf
σ σ' : ℝ
f : ℂ → ℂ
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
⊢ Tendsto (fun x => HIntegral f σ σ' (-x) - HIntegral f σ σ' x + VIntegral f σ' (-x) x) atTop
    (𝓝 (0 - 0 + VerticalIntegral f σ'))

State before:
case hf
σ σ' : ℝ
f : ℂ → ℂ
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
⊢ Tendsto (fun x => HIntegral f σ σ' (-x) - HIntegral f σ σ' x + VIntegral f σ' (-x) x) atTop
    (𝓝 (0 - 0 + VerticalIntegral f σ'))
Tactic:
apply Tendsto.add <| Tendsto.sub (hbot.comp tendsto_neg_atTop_atBot) htop
State after:
case hf
σ σ' : ℝ
f : ℂ → ℂ
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
⊢ Tendsto (fun x => VIntegral f σ' (-x) x) atTop (𝓝 (VerticalIntegral f σ'))

State before:
case hf
σ σ' : ℝ
f : ℂ → ℂ
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
⊢ Tendsto (fun x => VIntegral f σ' (-x) x) atTop (𝓝 (VerticalIntegral f σ'))
Tactic:
exact (intervalIntegral_tendsto_integral hright tendsto_neg_atTop_atBot tendsto_id).const_smul I
State after:
no goals

State before:
case hg
σ σ' : ℝ
f : ℂ → ℂ
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
⊢ Tendsto (fun x => VIntegral f σ (-x) x) atTop (𝓝 (VerticalIntegral f σ))
Tactic:
exact (intervalIntegral_tendsto_integral hleft tendsto_neg_atTop_atBot tendsto_id).const_smul I
State after:
no goals