internlm/Lean-Github huggingface dataset:
Theorem: RectangleIntegral_tendsTo_VerticalIntegral
Proof 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]
Proof 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 σ'))
Theorem: RectangleIntegral_tendsTo_VerticalIntegral
Proof 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
Proof 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 σ'))
Theorem: RectangleIntegral_tendsTo_VerticalIntegral
Proof 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
Proof state after:
no goals
Theorem: RectangleIntegral_tendsTo_VerticalIntegral
Proof 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
Proof state after:
no goals
Theorem: verticalIntegral_eq_verticalIntegral
Proof 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)
Proof 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}
Theorem: verticalIntegral_eq_verticalIntegral
Proof 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⟩)
Proof state after:
no goals
Theorem: verticalIntegral_eq_verticalIntegral
Proof 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
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
⊢ ∀ᶠ (c : ℝ) in 𝓝[>] 0,
    VerticalIntegral f σ' - VerticalIntegral f σ = RectangleIntegral f (-↑c - ↑c * I + p) (↑c + ↑c * I + p)
Tactic:
have : Icc σ σ' ×ℂ univ ∈ 𝓝 p := by
  rw [← mem_interior_iff_mem_nhds, Complex.interior_reProdIm, interior_Icc, interior_univ]
  refine ⟨⟨?_, ?_⟩, trivial⟩ <;> linarith
Proof state after:
σ σ' : ℝ
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 : ℝ) in 𝓝[>] 0,
    VerticalIntegral f σ' - VerticalIntegral f σ = RectangleIntegral f (-↑c - ↑c * I + p) (↑c + ↑c * I + p)
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 : ℝ) in 𝓝[>] 0,
    VerticalIntegral f σ' - VerticalIntegral f σ = RectangleIntegral f (-↑c - ↑c * I + p) (↑c + ↑c * I + p)
Tactic:
obtain ⟨c', hc'0, hc'⟩ := ((nhds_hasBasis_square p).1 _).mp this
Proof state after:
case intro.intro
σ σ' : ℝ
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 : ℝ) in 𝓝[>] 0,
    VerticalIntegral f σ' - VerticalIntegral f σ = RectangleIntegral f (-↑c - ↑c * I + p) (↑c + ↑c * I + p)
Theorem: verticalIntegral_sub_verticalIntegral_eq_squareIntegral
Proof state before:
case intro.intro
σ σ' : ℝ
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 : ℝ) in 𝓝[>] 0,
    VerticalIntegral f σ' - VerticalIntegral f σ = RectangleIntegral f (-↑c - ↑c * I + p) (↑c + ↑c * I + p)
Tactic:
filter_upwards [Ioo_mem_nhdsWithin_Ioi' hc'0] with c ⟨hc0, hcc'⟩
Proof state after:
case h
σ σ' : ℝ
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'
⊢ VerticalIntegral f σ' - VerticalIntegral f σ = RectangleIntegral f (-↑c - ↑c * I + p) (↑c + ↑c * I + p)
Theorem: verticalIntegral_sub_verticalIntegral_eq_squareIntegral
Proof state before:
case h
σ σ' : ℝ
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'
⊢ VerticalIntegral f σ' - VerticalIntegral f σ = RectangleIntegral f (-↑c - ↑c * I + p) (↑c + ↑c * I + p)
Tactic:
have hsub : Square p c ⊆ Icc σ σ' ×ℂ univ := (square_subset_square hc0 hcc'.le).trans hc'
Proof state after:
case h
σ σ' : ℝ
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
⊢ VerticalIntegral f σ' - VerticalIntegral f σ = RectangleIntegral f (-↑c - ↑c * I + p) (↑c + ↑c * I + p)
Theorem: verticalIntegral_sub_verticalIntegral_eq_squareIntegral
Proof state before:
case h
σ σ' : ℝ
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
⊢ VerticalIntegral f σ' - VerticalIntegral f σ = RectangleIntegral f (-↑c - ↑c * I + p) (↑c + ↑c * I + p)
Tactic:
apply tendsto_nhds_unique (RectangleIntegral_tendsTo_VerticalIntegral hbot htop hleft hright)
Proof state after:
case h
σ σ' : ℝ
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
⊢ Tendsto (fun T => RectangleIntegral f (↑σ - I * ↑T) (↑σ' + I * ↑T)) atTop
    (𝓝 (RectangleIntegral f (-↑c - ↑c * I + p) (↑c + ↑c * I + p)))
Theorem: verticalIntegral_sub_verticalIntegral_eq_squareIntegral
Proof state before:
case h
σ σ' : ℝ
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
⊢ Tendsto (fun T => RectangleIntegral f (↑σ - I * ↑T) (↑σ' + I * ↑T)) atTop
    (𝓝 (RectangleIntegral f (-↑c - ↑c * I + p) (↑c + ↑c * I + p)))
Tactic:
apply Filter.EventuallyEq.tendsto
Proof state after:
case h.hf
σ σ' : ℝ
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
⊢ (fun T => RectangleIntegral f (↑σ - I * ↑T) (↑σ' + I * ↑T)) =ᶠ[atTop] fun x =>
    RectangleIntegral f (-↑c - ↑c * I + p) (↑c + ↑c * I + p)
Theorem: verticalIntegral_sub_verticalIntegral_eq_squareIntegral
Proof state before:
case h.hf
σ σ' : ℝ
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
⊢ (fun T => RectangleIntegral f (↑σ - I * ↑T) (↑σ' + I * ↑T)) =ᶠ[atTop] fun x =>
    RectangleIntegral f (-↑c - ↑c * I + p) (↑c + ↑c * I + p)
Tactic:
filter_upwards [Filter.Ioi_mem_atTop ((c - p.im) ⊔ (c + p.im))] with y hy
Proof state after:
case h
σ σ' : ℝ
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))
⊢ RectangleIntegral f (↑σ - I * ↑y) (↑σ' + I * ↑y) = RectangleIntegral f (-↑c - ↑c * I + p) (↑c + ↑c * I + p)
Theorem: verticalIntegral_sub_verticalIntegral_eq_squareIntegral
Proof state before:
case h
σ σ' : ℝ
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))
⊢ RectangleIntegral f (↑σ - I * ↑y) (↑σ' + I * ↑y) = RectangleIntegral f (-↑c - ↑c * I + p) (↑c + ↑c * I + p)
Tactic:
have : c - p.im < y ∧ c + p.im < y := sup_lt_iff.mp hy
Proof state after:
case h
σ σ' : ℝ
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
⊢ RectangleIntegral f (↑σ - I * ↑y) (↑σ' + I * ↑y) = RectangleIntegral f (-↑c - ↑c * I + p) (↑c + ↑c * I + p)
Theorem: verticalIntegral_sub_verticalIntegral_eq_squareIntegral
Proof state before:
case h
σ σ' : ℝ
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
⊢ RectangleIntegral f (↑σ - I * ↑y) (↑σ' + I * ↑y) = RectangleIntegral f (-↑c - ↑c * I + p) (↑c + ↑c * I + p)
Tactic:
have : c + σ ≤ p.re := by simpa using (hsub ⟨left_mem_uIcc, left_mem_uIcc⟩).1.1
Proof state after:
case h
σ σ' : ℝ
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
⊢ RectangleIntegral f (↑σ - I * ↑y) (↑σ' + I * ↑y) = RectangleIntegral f (-↑c - ↑c * I + p) (↑c + ↑c * I + p)
Theorem: verticalIntegral_sub_verticalIntegral_eq_squareIntegral
Proof state before:
case h
σ σ' : ℝ
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
⊢ RectangleIntegral f (↑σ - I * ↑y) (↑σ' + I * ↑y) = RectangleIntegral f (-↑c - ↑c * I + p) (↑c + ↑c * I + p)
Tactic:
have : c + p.re ≤ σ' := by simpa using (hsub ⟨right_mem_uIcc, right_mem_uIcc⟩).1.2
Proof state after:
case h
σ σ' : ℝ
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 ≤ σ'
⊢ RectangleIntegral f (↑σ - I * ↑y) (↑σ' + I * ↑y) = RectangleIntegral f (-↑c - ↑c * I + p) (↑c + ↑c * I + p)
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
⊢ Icc σ σ' ×ℂ univ ∈ 𝓝 p
Tactic:
rw [← mem_interior_iff_mem_nhds, Complex.interior_reProdIm, interior_Icc, interior_univ]
Proof state after:
σ σ' : ℝ
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
⊢ p ∈ Ioo σ σ' ×ℂ univ
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
⊢ p ∈ Ioo σ σ' ×ℂ univ
Tactic:
refine ⟨⟨?_, ?_⟩, trivial⟩ <;> 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
⊢ c + σ ≤ p.re
Tactic:
simpa using (hsub ⟨left_mem_uIcc, left_mem_uIcc⟩).1.1
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
⊢ c + p.re ≤ σ'
Tactic:
simpa using (hsub ⟨right_mem_uIcc, right_mem_uIcc⟩).1.2
Proof state after:
no goals
Theorem: verticalIntegral_sub_verticalIntegral_eq_squareIntegral
Proof state before:
case h.h_orientation
σ σ' : ℝ
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 ≤ σ'
⊢ (↑σ - I * ↑y).re ≤ (↑σ' + I * ↑y).re ∧
    (↑σ - I * ↑y).im ≤ (↑σ' + I * ↑y).im ∧
      (-↑c - ↑c * I + p).re ≤ (↑c + ↑c * I + p).re ∧ (-↑c - ↑c * I + p).im ≤ (↑c + ↑c * I + p).im
Tactic:
simpa using ⟨by linarith, by linarith, by linarith⟩
Proof state after:
no goals