internlm/Lean-Github huggingface dataset:
Theorem: verticalIntegral_sub_verticalIntegral_eq_squareIntegral
Proof state before:
σ σ' : ℝ
f : ℂ → ℂ
p : ℂ
hσ : σ < p.re ∧ p.re < σ'
hf : HolomorphicOn f (Icc σ σ' ×ℂ univ \ {p})
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
this✝² : Icc σ σ' ×ℂ univ ∈ 𝓝 p
c' : ℝ
hc'0 : 0 < c'
hc' : Square p c' ⊆ Icc σ σ' ×ℂ univ
c : ℝ
hc0 : 0 < c
hcc' : c < c'
hsub : Square p c ⊆ Icc σ σ' ×ℂ univ
y : ℝ
hy : y ∈ Ioi ((c - p.im) ⊔ (c + p.im))
this✝¹ : c - p.im < y ∧ c + p.im < y
this✝ : c + σ ≤ p.re
this : c + p.re ≤ σ'
⊢ σ ≤ σ'
Tactic:
linarith
Proof state after:
no goals
Theorem: verticalIntegral_sub_verticalIntegral_eq_squareIntegral
Proof state before:
σ σ' : ℝ
f : ℂ → ℂ
p : ℂ
hσ : σ < p.re ∧ p.re < σ'
hf : HolomorphicOn f (Icc σ σ' ×ℂ univ \ {p})
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
this✝² : Icc σ σ' ×ℂ univ ∈ 𝓝 p
c' : ℝ
hc'0 : 0 < c'
hc' : Square p c' ⊆ Icc σ σ' ×ℂ univ
c : ℝ
hc0 : 0 < c
hcc' : c < c'
hsub : Square p c ⊆ Icc σ σ' ×ℂ univ
y : ℝ
hy : y ∈ Ioi ((c - p.im) ⊔ (c + p.im))
this✝¹ : c - p.im < y ∧ c + p.im < y
this✝ : c + σ ≤ p.re
this : c + p.re ≤ σ'
⊢ 0 ≤ y
Tactic:
linarith
Proof state after:
no goals
Theorem: verticalIntegral_sub_verticalIntegral_eq_squareIntegral
Proof state before:
σ σ' : ℝ
f : ℂ → ℂ
p : ℂ
hσ : σ < p.re ∧ p.re < σ'
hf : HolomorphicOn f (Icc σ σ' ×ℂ univ \ {p})
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
this✝² : Icc σ σ' ×ℂ univ ∈ 𝓝 p
c' : ℝ
hc'0 : 0 < c'
hc' : Square p c' ⊆ Icc σ σ' ×ℂ univ
c : ℝ
hc0 : 0 < c
hcc' : c < c'
hsub : Square p c ⊆ Icc σ σ' ×ℂ univ
y : ℝ
hy : y ∈ Ioi ((c - p.im) ⊔ (c + p.im))
this✝¹ : c - p.im < y ∧ c + p.im < y
this✝ : c + σ ≤ p.re
this : c + p.re ≤ σ'
⊢ 0 ≤ c
Tactic:
linarith
Proof state after:
no goals
Theorem: verticalIntegral_sub_verticalIntegral_eq_squareIntegral
Proof state before:
case h.hp
σ σ' : ℝ
f : ℂ → ℂ
p : ℂ
hσ : σ < p.re ∧ p.re < σ'
hf : HolomorphicOn f (Icc σ σ' ×ℂ univ \ {p})
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
this✝² : Icc σ σ' ×ℂ univ ∈ 𝓝 p
c' : ℝ
hc'0 : 0 < c'
hc' : Square p c' ⊆ Icc σ σ' ×ℂ univ
c : ℝ
hc0 : 0 < c
hcc' : c < c'
hsub : Square p c ⊆ Icc σ σ' ×ℂ univ
y : ℝ
hy : y ∈ Ioi ((c - p.im) ⊔ (c + p.im))
this✝¹ : c - p.im < y ∧ c + p.im < y
this✝ : c + σ ≤ p.re
this : c + p.re ≤ σ'
⊢ Rectangle (-↑c - ↑c * I + p) (↑c + ↑c * I + p) ∈ 𝓝 ?h.p
Tactic:
exact square_mem_nhds p (ne_of_gt hc0)
Proof state after:
no goals
Theorem: verticalIntegral_sub_verticalIntegral_eq_squareIntegral
Proof state before:
case h.hz
σ σ' : ℝ
f : ℂ → ℂ
p : ℂ
hσ : σ < p.re ∧ p.re < σ'
hf : HolomorphicOn f (Icc σ σ' ×ℂ univ \ {p})
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
this✝² : Icc σ σ' ×ℂ univ ∈ 𝓝 p
c' : ℝ
hc'0 : 0 < c'
hc' : Square p c' ⊆ Icc σ σ' ×ℂ univ
c : ℝ
hc0 : 0 < c
hcc' : c < c'
hsub : Square p c ⊆ Icc σ σ' ×ℂ univ
y : ℝ
hy : y ∈ Ioi ((c - p.im) ⊔ (c + p.im))
this✝¹ : c - p.im < y ∧ c + p.im < y
this✝ : c + σ ≤ p.re
this : c + p.re ≤ σ'
⊢ Rectangle (-↑c - ↑c * I + p) (↑c + ↑c * I + p) ⊆ Rectangle (↑σ - I * ↑y) (↑σ' + I * ↑y)
Tactic:
apply RectSubRect' <;> simpa using by linarith
Proof state after:
no goals
Theorem: verticalIntegral_sub_verticalIntegral_eq_squareIntegral
Proof state before:
σ σ' : ℝ
f : ℂ → ℂ
p : ℂ
hσ : σ < p.re ∧ p.re < σ'
hf : HolomorphicOn f (Icc σ σ' ×ℂ univ \ {p})
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
this✝² : Icc σ σ' ×ℂ univ ∈ 𝓝 p
c' : ℝ
hc'0 : 0 < c'
hc' : Square p c' ⊆ Icc σ σ' ×ℂ univ
c : ℝ
hc0 : 0 < c
hcc' : c < c'
hsub : Square p c ⊆ Icc σ σ' ×ℂ univ
y : ℝ
hy : y ∈ Ioi ((c - p.im) ⊔ (c + p.im))
this✝¹ : c - p.im < y ∧ c + p.im < y
this✝ : c + σ ≤ p.re
this : c + p.re ≤ σ'
⊢ c + p.im ≤ y
Tactic:
linarith
Proof state after:
no goals
Theorem: verticalIntegral_sub_verticalIntegral_eq_squareIntegral
Proof state before:
case h.fHolo
σ σ' : ℝ
f : ℂ → ℂ
p : ℂ
hσ : σ < p.re ∧ p.re < σ'
hf : HolomorphicOn f (Icc σ σ' ×ℂ univ \ {p})
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
this✝² : Icc σ σ' ×ℂ univ ∈ 𝓝 p
c' : ℝ
hc'0 : 0 < c'
hc' : Square p c' ⊆ Icc σ σ' ×ℂ univ
c : ℝ
hc0 : 0 < c
hcc' : c < c'
hsub : Square p c ⊆ Icc σ σ' ×ℂ univ
y : ℝ
hy : y ∈ Ioi ((c - p.im) ⊔ (c + p.im))
this✝¹ : c - p.im < y ∧ c + p.im < y
this✝ : c + σ ≤ p.re
this : c + p.re ≤ σ'
⊢ HolomorphicOn f (Rectangle (↑σ - I * ↑y) (↑σ' + I * ↑y) \ {p})
Tactic:
refine hf.mono (diff_subset_diff ?_ subset_rfl)
Proof state after:
case h.fHolo
σ σ' : ℝ
f : ℂ → ℂ
p : ℂ
hσ : σ < p.re ∧ p.re < σ'
hf : HolomorphicOn f (Icc σ σ' ×ℂ univ \ {p})
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
this✝² : Icc σ σ' ×ℂ univ ∈ 𝓝 p
c' : ℝ
hc'0 : 0 < c'
hc' : Square p c' ⊆ Icc σ σ' ×ℂ univ
c : ℝ
hc0 : 0 < c
hcc' : c < c'
hsub : Square p c ⊆ Icc σ σ' ×ℂ univ
y : ℝ
hy : y ∈ Ioi ((c - p.im) ⊔ (c + p.im))
this✝¹ : c - p.im < y ∧ c + p.im < y
this✝ : c + σ ≤ p.re
this : c + p.re ≤ σ'
⊢ Rectangle (↑σ - I * ↑y) (↑σ' + I * ↑y) ⊆ Icc σ σ' ×ℂ univ
Theorem: verticalIntegral_sub_verticalIntegral_eq_squareIntegral
Proof state before:
case h.fHolo
σ σ' : ℝ
f : ℂ → ℂ
p : ℂ
hσ : σ < p.re ∧ p.re < σ'
hf : HolomorphicOn f (Icc σ σ' ×ℂ univ \ {p})
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
this✝² : Icc σ σ' ×ℂ univ ∈ 𝓝 p
c' : ℝ
hc'0 : 0 < c'
hc' : Square p c' ⊆ Icc σ σ' ×ℂ univ
c : ℝ
hc0 : 0 < c
hcc' : c < c'
hsub : Square p c ⊆ Icc σ σ' ×ℂ univ
y : ℝ
hy : y ∈ Ioi ((c - p.im) ⊔ (c + p.im))
this✝¹ : c - p.im < y ∧ c + p.im < y
this✝ : c + σ ≤ p.re
this : c + p.re ≤ σ'
⊢ Rectangle (↑σ - I * ↑y) (↑σ' + I * ↑y) ⊆ Icc σ σ' ×ℂ univ
Tactic:
simpa [Rectangle, uIcc_of_lt (hσ.1.trans hσ.2)] using fun x ⟨hx, _⟩ ↦ ⟨hx, trivial⟩
Proof state after:
no goals
Theorem: RectangleIntegral_tendsTo_UpperU
Proof state before:
σ σ' T : ℝ
f : ℂ → ℂ
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 (𝓝 (UpperUIntegral f σ σ' T))
Tactic:
have h_re  (s : ℝ) (t : ℝ) : (s  + I * t).re = s  := by simp
Proof state after:
σ σ' T : ℝ
f : ℂ → ℂ
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
h_re : ∀ (s t : ℝ), (↑s + I * ↑t).re = s
⊢ Tendsto (fun U => RectangleIntegral f (↑σ + I * ↑T) (↑σ' + I * ↑U)) atTop (𝓝 (UpperUIntegral f σ σ' T))
Theorem: RectangleIntegral_tendsTo_UpperU
Proof state before:
σ σ' T : ℝ
f : ℂ → ℂ
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
h_re : ∀ (s t : ℝ), (↑s + I * ↑t).re = s
⊢ Tendsto (fun U => RectangleIntegral f (↑σ + I * ↑T) (↑σ' + I * ↑U)) atTop (𝓝 (UpperUIntegral f σ σ' T))
Tactic:
have h_im  (s : ℝ) (t : ℝ) : (s  + I * t).im = t  := by simp
Proof state after:
σ σ' T : ℝ
f : ℂ → ℂ
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
h_re : ∀ (s t : ℝ), (↑s + I * ↑t).re = s
h_im : ∀ (s t : ℝ), (↑s + I * ↑t).im = t
⊢ Tendsto (fun U => RectangleIntegral f (↑σ + I * ↑T) (↑σ' + I * ↑U)) atTop (𝓝 (UpperUIntegral f σ σ' T))
Theorem: RectangleIntegral_tendsTo_UpperU
Proof state before:
σ σ' T : ℝ
f : ℂ → ℂ
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
h_re : ∀ (s t : ℝ), (↑s + I * ↑t).re = s
h_im : ∀ (s t : ℝ), (↑s + I * ↑t).im = t
⊢ Tendsto (fun U => RectangleIntegral f (↑σ + I * ↑T) (↑σ' + I * ↑U)) atTop (𝓝 (UpperUIntegral f σ σ' T))
Tactic:
have hbot : Tendsto (fun (_ : ℝ) ↦ ∫ (x : ℝ) in σ..σ', f (x + T * I)) atTop (𝓝 <| ∫ (x : ℝ) in σ..σ', f (x + T * I)) := by
  exact tendsto_const_nhds
Proof state after:
σ σ' T : ℝ
f : ℂ → ℂ
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
h_re : ∀ (s t : ℝ), (↑s + I * ↑t).re = s
h_im : ∀ (s t : ℝ), (↑s + I * ↑t).im = t
hbot : Tendsto (fun x => ∫ (x : ℝ) in σ..σ', f (↑x + ↑T * I)) atTop (𝓝 (∫ (x : ℝ) in σ..σ', f (↑x + ↑T * I)))
⊢ Tendsto (fun U => RectangleIntegral f (↑σ + I * ↑T) (↑σ' + I * ↑U)) atTop (𝓝 (UpperUIntegral f σ σ' T))
Theorem: RectangleIntegral_tendsTo_UpperU
Proof state before:
σ σ' T : ℝ
f : ℂ → ℂ
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
h_re : ∀ (s t : ℝ), (↑s + I * ↑t).re = s
h_im : ∀ (s t : ℝ), (↑s + I * ↑t).im = t
hbot : Tendsto (fun x => ∫ (x : ℝ) in σ..σ', f (↑x + ↑T * I)) atTop (𝓝 (∫ (x : ℝ) in σ..σ', f (↑x + ↑T * I)))
⊢ Tendsto (fun U => RectangleIntegral f (↑σ + I * ↑T) (↑σ' + I * ↑U)) atTop (𝓝 (UpperUIntegral f σ σ' T))
Tactic:
have hvert (s : ℝ) (int : Integrable (fun (y : ℝ) ↦ f (s + y * I))) :
    Tendsto (fun (U : ℝ) ↦ I * ∫ (y : ℝ) in T..U, f (s + y * I)) atTop (𝓝 <| I * ∫ (y : ℝ) in Ioi T, f (s + y * I)) := by
  exact (intervalIntegral_tendsto_integral_Ioi T int.restrict tendsto_id).const_smul I
Proof state after:
σ σ' T : ℝ
f : ℂ → ℂ
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
h_re : ∀ (s t : ℝ), (↑s + I * ↑t).re = s
h_im : ∀ (s t : ℝ), (↑s + I * ↑t).im = t
hbot : Tendsto (fun x => ∫ (x : ℝ) in σ..σ', f (↑x + ↑T * I)) atTop (𝓝 (∫ (x : ℝ) in σ..σ', f (↑x + ↑T * I)))
hvert :
  ∀ (s : ℝ),
    Integrable (fun y => f (↑s + ↑y * I)) volume →
      Tendsto (fun U => I * ∫ (y : ℝ) in T..U, f (↑s + ↑y * I)) atTop (𝓝 (I * ∫ (y : ℝ) in Ioi T, f (↑s + ↑y * I)))
⊢ Tendsto (fun U => RectangleIntegral f (↑σ + I * ↑T) (↑σ' + I * ↑U)) atTop (𝓝 (UpperUIntegral f σ σ' T))
Theorem: RectangleIntegral_tendsTo_UpperU
Proof state before:
σ σ' T : ℝ
f : ℂ → ℂ
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
h_re : ∀ (s t : ℝ), (↑s + I * ↑t).re = s
h_im : ∀ (s t : ℝ), (↑s + I * ↑t).im = t
hbot : Tendsto (fun x => ∫ (x : ℝ) in σ..σ', f (↑x + ↑T * I)) atTop (𝓝 (∫ (x : ℝ) in σ..σ', f (↑x + ↑T * I)))
hvert :
  ∀ (s : ℝ),
    Integrable (fun y => f (↑s + ↑y * I)) volume →
      Tendsto (fun U => I * ∫ (y : ℝ) in T..U, f (↑s + ↑y * I)) atTop (𝓝 (I * ∫ (y : ℝ) in Ioi T, f (↑s + ↑y * I)))
⊢ Tendsto (fun U => RectangleIntegral f (↑σ + I * ↑T) (↑σ' + I * ↑U)) atTop (𝓝 (UpperUIntegral f σ σ' T))
Tactic:
have := ((hbot.sub htop).add (hvert σ' hright)).sub (hvert σ hleft)
Proof state after:
σ σ' T : ℝ
f : ℂ → ℂ
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
h_re : ∀ (s t : ℝ), (↑s + I * ↑t).re = s
h_im : ∀ (s t : ℝ), (↑s + I * ↑t).im = t
hbot : Tendsto (fun x => ∫ (x : ℝ) in σ..σ', f (↑x + ↑T * I)) atTop (𝓝 (∫ (x : ℝ) in σ..σ', f (↑x + ↑T * I)))
hvert :
  ∀ (s : ℝ),
    Integrable (fun y => f (↑s + ↑y * I)) volume →
      Tendsto (fun U => I * ∫ (y : ℝ) in T..U, f (↑s + ↑y * I)) atTop (𝓝 (I * ∫ (y : ℝ) in Ioi T, f (↑s + ↑y * I)))
this :
  Tendsto
    (fun x =>
      (((∫ (x : ℝ) in σ..σ', f (↑x + ↑T * I)) - ∫ (x_1 : ℝ) in σ..σ', f (↑x_1 + ↑x * I)) +
          I * ∫ (y : ℝ) in T..x, f (↑σ' + ↑y * I)) -
        I * ∫ (y : ℝ) in T..x, f (↑σ + ↑y * I))
    atTop
    (𝓝
      (((∫ (x : ℝ) in σ..σ', f (↑x + ↑T * I)) - 0 + I * ∫ (y : ℝ) in Ioi T, f (↑σ' + ↑y * I)) -
        I * ∫ (y : ℝ) in Ioi T, f (↑σ + ↑y * I)))
⊢ Tendsto (fun U => RectangleIntegral f (↑σ + I * ↑T) (↑σ' + I * ↑U)) atTop (𝓝 (UpperUIntegral f σ σ' T))
Theorem: RectangleIntegral_tendsTo_UpperU
Proof state before:
σ σ' T : ℝ
f : ℂ → ℂ
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
h_re : ∀ (s t : ℝ), (↑s + I * ↑t).re = s
h_im : ∀ (s t : ℝ), (↑s + I * ↑t).im = t
hbot : Tendsto (fun x => ∫ (x : ℝ) in σ..σ', f (↑x + ↑T * I)) atTop (𝓝 (∫ (x : ℝ) in σ..σ', f (↑x + ↑T * I)))
hvert :
  ∀ (s : ℝ),
    Integrable (fun y => f (↑s + ↑y * I)) volume →
      Tendsto (fun U => I * ∫ (y : ℝ) in T..U, f (↑s + ↑y * I)) atTop (𝓝 (I * ∫ (y : ℝ) in Ioi T, f (↑s + ↑y * I)))
this :
  Tendsto
    (fun x =>
      (((∫ (x : ℝ) in σ..σ', f (↑x + ↑T * I)) - ∫ (x_1 : ℝ) in σ..σ', f (↑x_1 + ↑x * I)) +
          I * ∫ (y : ℝ) in T..x, f (↑σ' + ↑y * I)) -
        I * ∫ (y : ℝ) in T..x, f (↑σ + ↑y * I))
    atTop
    (𝓝
      (((∫ (x : ℝ) in σ..σ', f (↑x + ↑T * I)) - 0 + I * ∫ (y : ℝ) in Ioi T, f (↑σ' + ↑y * I)) -
        I * ∫ (y : ℝ) in Ioi T, f (↑σ + ↑y * I)))
⊢ Tendsto (fun U => RectangleIntegral f (↑σ + I * ↑T) (↑σ' + I * ↑U)) atTop (𝓝 (UpperUIntegral f σ σ' T))
Tactic:
simpa only [RectangleIntegral, UpperUIntegral, h_re, h_im, sub_zero, ←integral_Ici_eq_integral_Ioi]
Proof state after:
no goals
Theorem: RectangleIntegral_tendsTo_UpperU
Proof state before:
σ σ' T : ℝ
f : ℂ → ℂ
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
s t : ℝ
⊢ (↑s + I * ↑t).re = s
Tactic:
simp
Proof state after:
no goals
Theorem: RectangleIntegral_tendsTo_UpperU
Proof state before:
σ σ' T : ℝ
f : ℂ → ℂ
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
h_re : ∀ (s t : ℝ), (↑s + I * ↑t).re = s
s t : ℝ
⊢ (↑s + I * ↑t).im = t
Tactic:
simp
Proof state after:
no goals
Theorem: RectangleIntegral_tendsTo_UpperU
Proof state before:
σ σ' T : ℝ
f : ℂ → ℂ
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
h_re : ∀ (s t : ℝ), (↑s + I * ↑t).re = s
h_im : ∀ (s t : ℝ), (↑s + I * ↑t).im = t
⊢ Tendsto (fun x => ∫ (x : ℝ) in σ..σ', f (↑x + ↑T * I)) atTop (𝓝 (∫ (x : ℝ) in σ..σ', f (↑x + ↑T * I)))
Tactic:
exact tendsto_const_nhds
Proof state after:
no goals
Theorem: RectangleIntegral_tendsTo_UpperU
Proof state before:
σ σ' T : ℝ
f : ℂ → ℂ
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
h_re : ∀ (s t : ℝ), (↑s + I * ↑t).re = s
h_im : ∀ (s t : ℝ), (↑s + I * ↑t).im = t
hbot : Tendsto (fun x => ∫ (x : ℝ) in σ..σ', f (↑x + ↑T * I)) atTop (𝓝 (∫ (x : ℝ) in σ..σ', f (↑x + ↑T * I)))
s : ℝ
int : Integrable (fun y => f (↑s + ↑y * I)) volume
⊢ Tendsto (fun U => I * ∫ (y : ℝ) in T..U, f (↑s + ↑y * I)) atTop (𝓝 (I * ∫ (y : ℝ) in Ioi T, f (↑s + ↑y * I)))
Tactic:
exact (intervalIntegral_tendsto_integral_Ioi T int.restrict tendsto_id).const_smul I
Proof state after:
no goals
Theorem: RectangleIntegral_tendsTo_LowerU
Proof state before:
σ σ' T : ℝ
f : ℂ → ℂ
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 (𝓝 (-LowerUIntegral f σ σ' T))
Tactic:
have h_re  (s : ℝ) (t : ℝ) : (s  - I * t).re = s  := by simp
Proof state after:
σ σ' T : ℝ
f : ℂ → ℂ
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_re : ∀ (s t : ℝ), (↑s - I * ↑t).re = s
⊢ Tendsto (fun U => RectangleIntegral f (↑σ - I * ↑U) (↑σ' - I * ↑T)) atTop (𝓝 (-LowerUIntegral f σ σ' T))
Theorem: RectangleIntegral_tendsTo_LowerU
Proof state before:
σ σ' T : ℝ
f : ℂ → ℂ
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_re : ∀ (s t : ℝ), (↑s - I * ↑t).re = s
⊢ Tendsto (fun U => RectangleIntegral f (↑σ - I * ↑U) (↑σ' - I * ↑T)) atTop (𝓝 (-LowerUIntegral f σ σ' T))
Tactic:
have h_im  (s : ℝ) (t : ℝ) : (s  - I * t).im = -t  := by simp
Proof state after:
σ σ' T : ℝ
f : ℂ → ℂ
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_re : ∀ (s t : ℝ), (↑s - I * ↑t).re = s
h_im : ∀ (s t : ℝ), (↑s - I * ↑t).im = -t
⊢ Tendsto (fun U => RectangleIntegral f (↑σ - I * ↑U) (↑σ' - I * ↑T)) atTop (𝓝 (-LowerUIntegral f σ σ' T))
Theorem: RectangleIntegral_tendsTo_LowerU
Proof state before:
σ σ' T : ℝ
f : ℂ → ℂ
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_re : ∀ (s t : ℝ), (↑s - I * ↑t).re = s
h_im : ∀ (s t : ℝ), (↑s - I * ↑t).im = -t
⊢ Tendsto (fun U => RectangleIntegral f (↑σ - I * ↑U) (↑σ' - I * ↑T)) atTop (𝓝 (-LowerUIntegral f σ σ' T))
Tactic:
have hbot' : Tendsto (fun (y : ℝ) ↦ ∫ (x : ℝ) in σ..σ', f (x - y * I)) atTop (𝓝 0) := by
  convert (hbot.comp tendsto_neg_atTop_atBot) using 1
  ext; simp only [Function.comp_apply, ofReal_neg, neg_mul]; rfl
Proof state after:
σ σ' T : ℝ
f : ℂ → ℂ
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_re : ∀ (s t : ℝ), (↑s - I * ↑t).re = s
h_im : ∀ (s t : ℝ), (↑s - I * ↑t).im = -t
hbot' : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x - ↑y * I)) atTop (𝓝 0)
⊢ Tendsto (fun U => RectangleIntegral f (↑σ - I * ↑U) (↑σ' - I * ↑T)) atTop (𝓝 (-LowerUIntegral f σ σ' T))
Theorem: RectangleIntegral_tendsTo_LowerU
Proof state before:
σ σ' T : ℝ
f : ℂ → ℂ
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_re : ∀ (s t : ℝ), (↑s - I * ↑t).re = s
h_im : ∀ (s t : ℝ), (↑s - I * ↑t).im = -t
hbot' : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x - ↑y * I)) atTop (𝓝 0)
⊢ Tendsto (fun U => RectangleIntegral f (↑σ - I * ↑U) (↑σ' - I * ↑T)) atTop (𝓝 (-LowerUIntegral f σ σ' T))
Tactic:
have htop : Tendsto (fun (_ : ℝ) ↦ ∫ (x : ℝ) in σ..σ', f (x - T * I)) atTop (𝓝 <| ∫ (x : ℝ) in σ..σ', f (x - T * I)) :=
  tendsto_const_nhds
Proof state after:
σ σ' T : ℝ
f : ℂ → ℂ
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_re : ∀ (s t : ℝ), (↑s - I * ↑t).re = s
h_im : ∀ (s t : ℝ), (↑s - I * ↑t).im = -t
hbot' : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x - ↑y * I)) atTop (𝓝 0)
htop : Tendsto (fun x => ∫ (x : ℝ) in σ..σ', f (↑x - ↑T * I)) atTop (𝓝 (∫ (x : ℝ) in σ..σ', f (↑x - ↑T * I)))
⊢ Tendsto (fun U => RectangleIntegral f (↑σ - I * ↑U) (↑σ' - I * ↑T)) atTop (𝓝 (-LowerUIntegral f σ σ' T))
Theorem: RectangleIntegral_tendsTo_LowerU
Proof state before:
σ σ' T : ℝ
f : ℂ → ℂ
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_re : ∀ (s t : ℝ), (↑s - I * ↑t).re = s
h_im : ∀ (s t : ℝ), (↑s - I * ↑t).im = -t
hbot' : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x - ↑y * I)) atTop (𝓝 0)
htop : Tendsto (fun x => ∫ (x : ℝ) in σ..σ', f (↑x - ↑T * I)) atTop (𝓝 (∫ (x : ℝ) in σ..σ', f (↑x - ↑T * I)))
⊢ Tendsto (fun U => RectangleIntegral f (↑σ - I * ↑U) (↑σ' - I * ↑T)) atTop (𝓝 (-LowerUIntegral f σ σ' T))
Tactic:
have hvert (s : ℝ) (int : Integrable (fun (y : ℝ) ↦ f (s + y * I))) :
    Tendsto (fun (U : ℝ) ↦ I * ∫ (y : ℝ) in -U..-T, f (s + y * I)) atTop (𝓝 <| I * ∫ (y : ℝ) in Iic (-T), f (s + y * I)) := by
  have := (intervalIntegral_tendsto_integral_Iic (-T) int.restrict tendsto_id).const_smul I
  convert (this.comp tendsto_neg_atTop_atBot) using 1
Proof state after:
σ σ' T : ℝ
f : ℂ → ℂ
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_re : ∀ (s t : ℝ), (↑s - I * ↑t).re = s
h_im : ∀ (s t : ℝ), (↑s - I * ↑t).im = -t
hbot' : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x - ↑y * I)) atTop (𝓝 0)
htop : Tendsto (fun x => ∫ (x : ℝ) in σ..σ', f (↑x - ↑T * I)) atTop (𝓝 (∫ (x : ℝ) in σ..σ', f (↑x - ↑T * I)))
hvert :
  ∀ (s : ℝ),
    Integrable (fun y => f (↑s + ↑y * I)) volume →
      Tendsto (fun U => I * ∫ (y : ℝ) in -U..-T, f (↑s + ↑y * I)) atTop (𝓝 (I * ∫ (y : ℝ) in Iic (-T), f (↑s + ↑y * I)))
⊢ Tendsto (fun U => RectangleIntegral f (↑σ - I * ↑U) (↑σ' - I * ↑T)) atTop (𝓝 (-LowerUIntegral f σ σ' T))