internlm/Lean-Github huggingface dataset:
Theorem: ResidueTheoremOnRectangleWithSimplePole
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f✝ g✝ : ℂ → E
z✝ w✝ p✝ c A✝ : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
f g : ℂ → ℂ
z w p A : ℂ
zRe_le_wRe : z.re ≤ w.re
zIm_le_wIm : z.im ≤ w.im
pInRectInterior : Rectangle z w ∈ 𝓝 p
gHolo : HolomorphicOn g (Rectangle z w)
principalPart : EqOn (f - fun s => A / (s - p)) g (Rectangle z w \ {p})
principalPart' : EqOn f (g + fun s => A / (s - p)) (Rectangle z w \ {p})
this : EqOn f (g + fun s => A / (s - p)) (RectangleBorder z w)
t1 : RectangleBorderIntegrable g z w
t2 : HolomorphicOn (fun s => A / (s - p)) (Rectangle z w \ {p})
⊢ RectangleIntegral' (g + fun s => A / (s - p)) z w = A
Tactic:
have t3 : RectangleBorderIntegrable (fun s ↦ A / (s - p)) z w :=
  HolomorphicOn.rectangleBorderIntegrable' t2 pInRectInterior
Proof state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f✝ g✝ : ℂ → E
z✝ w✝ p✝ c A✝ : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
f g : ℂ → ℂ
z w p A : ℂ
zRe_le_wRe : z.re ≤ w.re
zIm_le_wIm : z.im ≤ w.im
pInRectInterior : Rectangle z w ∈ 𝓝 p
gHolo : HolomorphicOn g (Rectangle z w)
principalPart : EqOn (f - fun s => A / (s - p)) g (Rectangle z w \ {p})
principalPart' : EqOn f (g + fun s => A / (s - p)) (Rectangle z w \ {p})
this : EqOn f (g + fun s => A / (s - p)) (RectangleBorder z w)
t1 : RectangleBorderIntegrable g z w
t2 : HolomorphicOn (fun s => A / (s - p)) (Rectangle z w \ {p})
t3 : RectangleBorderIntegrable (fun s => A / (s - p)) z w
⊢ RectangleIntegral' (g + fun s => A / (s - p)) z w = A
Theorem: ResidueTheoremOnRectangleWithSimplePole
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f✝ g✝ : ℂ → E
z✝ w✝ p✝ c A✝ : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
f g : ℂ → ℂ
z w p A : ℂ
zRe_le_wRe : z.re ≤ w.re
zIm_le_wIm : z.im ≤ w.im
pInRectInterior : Rectangle z w ∈ 𝓝 p
gHolo : HolomorphicOn g (Rectangle z w)
principalPart : EqOn (f - fun s => A / (s - p)) g (Rectangle z w \ {p})
principalPart' : EqOn f (g + fun s => A / (s - p)) (Rectangle z w \ {p})
this : EqOn f (g + fun s => A / (s - p)) (RectangleBorder z w)
t1 : RectangleBorderIntegrable g z w
t2 : HolomorphicOn (fun s => A / (s - p)) (Rectangle z w \ {p})
t3 : RectangleBorderIntegrable (fun s => A / (s - p)) z w
⊢ RectangleIntegral' (g + fun s => A / (s - p)) z w = A
Tactic:
rw [RectangleIntegral', RectangleBorderIntegrable.add t1 t3, smul_add]
Proof state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f✝ g✝ : ℂ → E
z✝ w✝ p✝ c A✝ : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
f g : ℂ → ℂ
z w p A : ℂ
zRe_le_wRe : z.re ≤ w.re
zIm_le_wIm : z.im ≤ w.im
pInRectInterior : Rectangle z w ∈ 𝓝 p
gHolo : HolomorphicOn g (Rectangle z w)
principalPart : EqOn (f - fun s => A / (s - p)) g (Rectangle z w \ {p})
principalPart' : EqOn f (g + fun s => A / (s - p)) (Rectangle z w \ {p})
this : EqOn f (g + fun s => A / (s - p)) (RectangleBorder z w)
t1 : RectangleBorderIntegrable g z w
t2 : HolomorphicOn (fun s => A / (s - p)) (Rectangle z w \ {p})
t3 : RectangleBorderIntegrable (fun s => A / (s - p)) z w
⊢ (1 / (2 * ↑π * I)) • RectangleIntegral g z w + (1 / (2 * ↑π * I)) • RectangleIntegral (fun s => A / (s - p)) z w = A
Theorem: ResidueTheoremOnRectangleWithSimplePole
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f✝ g✝ : ℂ → E
z✝ w✝ p✝ c A✝ : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
f g : ℂ → ℂ
z w p A : ℂ
zRe_le_wRe : z.re ≤ w.re
zIm_le_wIm : z.im ≤ w.im
pInRectInterior : Rectangle z w ∈ 𝓝 p
gHolo : HolomorphicOn g (Rectangle z w)
principalPart : EqOn (f - fun s => A / (s - p)) g (Rectangle z w \ {p})
principalPart' : EqOn f (g + fun s => A / (s - p)) (Rectangle z w \ {p})
this : EqOn f (g + fun s => A / (s - p)) (RectangleBorder z w)
t1 : RectangleBorderIntegrable g z w
t2 : HolomorphicOn (fun s => A / (s - p)) (Rectangle z w \ {p})
t3 : RectangleBorderIntegrable (fun s => A / (s - p)) z w
⊢ (1 / (2 * ↑π * I)) • RectangleIntegral g z w + (1 / (2 * ↑π * I)) • RectangleIntegral (fun s => A / (s - p)) z w = A
Tactic:
rw [gHolo.vanishesOnRectangle (by rfl), smul_zero, zero_add]
Proof state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f✝ g✝ : ℂ → E
z✝ w✝ p✝ c A✝ : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
f g : ℂ → ℂ
z w p A : ℂ
zRe_le_wRe : z.re ≤ w.re
zIm_le_wIm : z.im ≤ w.im
pInRectInterior : Rectangle z w ∈ 𝓝 p
gHolo : HolomorphicOn g (Rectangle z w)
principalPart : EqOn (f - fun s => A / (s - p)) g (Rectangle z w \ {p})
principalPart' : EqOn f (g + fun s => A / (s - p)) (Rectangle z w \ {p})
this : EqOn f (g + fun s => A / (s - p)) (RectangleBorder z w)
t1 : RectangleBorderIntegrable g z w
t2 : HolomorphicOn (fun s => A / (s - p)) (Rectangle z w \ {p})
t3 : RectangleBorderIntegrable (fun s => A / (s - p)) z w
⊢ (1 / (2 * ↑π * I)) • RectangleIntegral (fun s => A / (s - p)) z w = A
Theorem: ResidueTheoremOnRectangleWithSimplePole
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f✝ g✝ : ℂ → E
z✝ w✝ p✝ c A✝ : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
f g : ℂ → ℂ
z w p A : ℂ
zRe_le_wRe : z.re ≤ w.re
zIm_le_wIm : z.im ≤ w.im
pInRectInterior : Rectangle z w ∈ 𝓝 p
gHolo : HolomorphicOn g (Rectangle z w)
principalPart : EqOn (f - fun s => A / (s - p)) g (Rectangle z w \ {p})
principalPart' : EqOn f (g + fun s => A / (s - p)) (Rectangle z w \ {p})
this : EqOn f (g + fun s => A / (s - p)) (RectangleBorder z w)
t1 : RectangleBorderIntegrable g z w
t2 : HolomorphicOn (fun s => A / (s - p)) (Rectangle z w \ {p})
t3 : RectangleBorderIntegrable (fun s => A / (s - p)) z w
⊢ (1 / (2 * ↑π * I)) • RectangleIntegral (fun s => A / (s - p)) z w = A
Tactic:
exact ResidueTheoremInRectangle zRe_le_wRe zIm_le_wIm pInRectInterior
Proof state after:
no goals
Theorem: ResidueTheoremOnRectangleWithSimplePole
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f✝ g✝ : ℂ → E
z✝ w✝ p✝ c A✝ : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
f g : ℂ → ℂ
z w p A : ℂ
zRe_le_wRe : z.re ≤ w.re
zIm_le_wIm : z.im ≤ w.im
pInRectInterior : Rectangle z w ∈ 𝓝 p
gHolo : HolomorphicOn g (Rectangle z w)
principalPart : EqOn (f - fun s => A / (s - p)) g (Rectangle z w \ {p})
s : ℂ
hs : s ∈ Rectangle z w \ {p}
⊢ f s = (g + fun s => A / (s - p)) s
Tactic:
rw [Pi.add_apply, ← principalPart hs, Pi.sub_apply, sub_add_cancel]
Proof state after:
no goals
Theorem: ResidueTheoremOnRectangleWithSimplePole
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f✝ g✝ : ℂ → E
z✝ w✝ p✝ c A✝ : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
f g : ℂ → ℂ
z w p A : ℂ
zRe_le_wRe : z.re ≤ w.re
zIm_le_wIm : z.im ≤ w.im
pInRectInterior : Rectangle z w ∈ 𝓝 p
gHolo : HolomorphicOn g (Rectangle z w)
principalPart : EqOn (f - fun s => A / (s - p)) g (Rectangle z w \ {p})
principalPart' : EqOn f (g + fun s => A / (s - p)) (Rectangle z w \ {p})
this : EqOn f (g + fun s => A / (s - p)) (RectangleBorder z w)
t1 : RectangleBorderIntegrable g z w
⊢ HolomorphicOn (fun s => A / (s - p)) (Rectangle z w \ {p})
Tactic:
apply DifferentiableOn.mono (t := {p}ᶜ)
Proof state after:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f✝ g✝ : ℂ → E
z✝ w✝ p✝ c A✝ : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
f g : ℂ → ℂ
z w p A : ℂ
zRe_le_wRe : z.re ≤ w.re
zIm_le_wIm : z.im ≤ w.im
pInRectInterior : Rectangle z w ∈ 𝓝 p
gHolo : HolomorphicOn g (Rectangle z w)
principalPart : EqOn (f - fun s => A / (s - p)) g (Rectangle z w \ {p})
principalPart' : EqOn f (g + fun s => A / (s - p)) (Rectangle z w \ {p})
this : EqOn f (g + fun s => A / (s - p)) (RectangleBorder z w)
t1 : RectangleBorderIntegrable g z w
⊢ DifferentiableOn ℂ (fun s => A / (s - p)) {p}ᶜ

case st
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f✝ g✝ : ℂ → E
z✝ w✝ p✝ c A✝ : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
f g : ℂ → ℂ
z w p A : ℂ
zRe_le_wRe : z.re ≤ w.re
zIm_le_wIm : z.im ≤ w.im
pInRectInterior : Rectangle z w ∈ 𝓝 p
gHolo : HolomorphicOn g (Rectangle z w)
principalPart : EqOn (f - fun s => A / (s - p)) g (Rectangle z w \ {p})
principalPart' : EqOn f (g + fun s => A / (s - p)) (Rectangle z w \ {p})
this : EqOn f (g + fun s => A / (s - p)) (RectangleBorder z w)
t1 : RectangleBorderIntegrable g z w
⊢ Rectangle z w \ {p} ⊆ {p}ᶜ
Theorem: ResidueTheoremOnRectangleWithSimplePole
Proof state before:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f✝ g✝ : ℂ → E
z✝ w✝ p✝ c A✝ : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
f g : ℂ → ℂ
z w p A : ℂ
zRe_le_wRe : z.re ≤ w.re
zIm_le_wIm : z.im ≤ w.im
pInRectInterior : Rectangle z w ∈ 𝓝 p
gHolo : HolomorphicOn g (Rectangle z w)
principalPart : EqOn (f - fun s => A / (s - p)) g (Rectangle z w \ {p})
principalPart' : EqOn f (g + fun s => A / (s - p)) (Rectangle z w \ {p})
this : EqOn f (g + fun s => A / (s - p)) (RectangleBorder z w)
t1 : RectangleBorderIntegrable g z w
⊢ DifferentiableOn ℂ (fun s => A / (s - p)) {p}ᶜ
Tactic:
apply DifferentiableOn.div
Proof state after:
case h.hc
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f✝ g✝ : ℂ → E
z✝ w✝ p✝ c A✝ : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
f g : ℂ → ℂ
z w p A : ℂ
zRe_le_wRe : z.re ≤ w.re
zIm_le_wIm : z.im ≤ w.im
pInRectInterior : Rectangle z w ∈ 𝓝 p
gHolo : HolomorphicOn g (Rectangle z w)
principalPart : EqOn (f - fun s => A / (s - p)) g (Rectangle z w \ {p})
principalPart' : EqOn f (g + fun s => A / (s - p)) (Rectangle z w \ {p})
this : EqOn f (g + fun s => A / (s - p)) (RectangleBorder z w)
t1 : RectangleBorderIntegrable g z w
⊢ DifferentiableOn ℂ (fun x => A) {p}ᶜ

case h.hd
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f✝ g✝ : ℂ → E
z✝ w✝ p✝ c A✝ : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
f g : ℂ → ℂ
z w p A : ℂ
zRe_le_wRe : z.re ≤ w.re
zIm_le_wIm : z.im ≤ w.im
pInRectInterior : Rectangle z w ∈ 𝓝 p
gHolo : HolomorphicOn g (Rectangle z w)
principalPart : EqOn (f - fun s => A / (s - p)) g (Rectangle z w \ {p})
principalPart' : EqOn f (g + fun s => A / (s - p)) (Rectangle z w \ {p})
this : EqOn f (g + fun s => A / (s - p)) (RectangleBorder z w)
t1 : RectangleBorderIntegrable g z w
⊢ DifferentiableOn ℂ (fun x => x - p) {p}ᶜ

case h.hx
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f✝ g✝ : ℂ → E
z✝ w✝ p✝ c A✝ : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
f g : ℂ → ℂ
z w p A : ℂ
zRe_le_wRe : z.re ≤ w.re
zIm_le_wIm : z.im ≤ w.im
pInRectInterior : Rectangle z w ∈ 𝓝 p
gHolo : HolomorphicOn g (Rectangle z w)
principalPart : EqOn (f - fun s => A / (s - p)) g (Rectangle z w \ {p})
principalPart' : EqOn f (g + fun s => A / (s - p)) (Rectangle z w \ {p})
this : EqOn f (g + fun s => A / (s - p)) (RectangleBorder z w)
t1 : RectangleBorderIntegrable g z w
⊢ ∀ x ∈ {p}ᶜ, x - p ≠ 0
Theorem: ResidueTheoremOnRectangleWithSimplePole
Proof state before:
case h.hc
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f✝ g✝ : ℂ → E
z✝ w✝ p✝ c A✝ : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
f g : ℂ → ℂ
z w p A : ℂ
zRe_le_wRe : z.re ≤ w.re
zIm_le_wIm : z.im ≤ w.im
pInRectInterior : Rectangle z w ∈ 𝓝 p
gHolo : HolomorphicOn g (Rectangle z w)
principalPart : EqOn (f - fun s => A / (s - p)) g (Rectangle z w \ {p})
principalPart' : EqOn f (g + fun s => A / (s - p)) (Rectangle z w \ {p})
this : EqOn f (g + fun s => A / (s - p)) (RectangleBorder z w)
t1 : RectangleBorderIntegrable g z w
⊢ DifferentiableOn ℂ (fun x => A) {p}ᶜ
Tactic:
exact differentiableOn_const _
Proof state after:
no goals
Theorem: ResidueTheoremOnRectangleWithSimplePole
Proof state before:
case h.hd
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f✝ g✝ : ℂ → E
z✝ w✝ p✝ c A✝ : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
f g : ℂ → ℂ
z w p A : ℂ
zRe_le_wRe : z.re ≤ w.re
zIm_le_wIm : z.im ≤ w.im
pInRectInterior : Rectangle z w ∈ 𝓝 p
gHolo : HolomorphicOn g (Rectangle z w)
principalPart : EqOn (f - fun s => A / (s - p)) g (Rectangle z w \ {p})
principalPart' : EqOn f (g + fun s => A / (s - p)) (Rectangle z w \ {p})
this : EqOn f (g + fun s => A / (s - p)) (RectangleBorder z w)
t1 : RectangleBorderIntegrable g z w
⊢ DifferentiableOn ℂ (fun x => x - p) {p}ᶜ
Tactic:
exact DifferentiableOn.sub differentiableOn_id (differentiableOn_const _)
Proof state after:
no goals
Theorem: ResidueTheoremOnRectangleWithSimplePole
Proof state before:
case h.hx
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f✝ g✝ : ℂ → E
z✝ w✝ p✝ c A✝ : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
f g : ℂ → ℂ
z w p A : ℂ
zRe_le_wRe : z.re ≤ w.re
zIm_le_wIm : z.im ≤ w.im
pInRectInterior : Rectangle z w ∈ 𝓝 p
gHolo : HolomorphicOn g (Rectangle z w)
principalPart : EqOn (f - fun s => A / (s - p)) g (Rectangle z w \ {p})
principalPart' : EqOn f (g + fun s => A / (s - p)) (Rectangle z w \ {p})
this : EqOn f (g + fun s => A / (s - p)) (RectangleBorder z w)
t1 : RectangleBorderIntegrable g z w
⊢ ∀ x ∈ {p}ᶜ, x - p ≠ 0
Tactic:
exact fun x hx => by rw [sub_ne_zero]; exact hx
Proof state after:
no goals
Theorem: ResidueTheoremOnRectangleWithSimplePole
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f✝ g✝ : ℂ → E
z✝ w✝ p✝ c A✝ : ℂ
x✝ x₁ x₂ y y₁ y₂ σ : ℝ
f g : ℂ → ℂ
z w p A : ℂ
zRe_le_wRe : z.re ≤ w.re
zIm_le_wIm : z.im ≤ w.im
pInRectInterior : Rectangle z w ∈ 𝓝 p
gHolo : HolomorphicOn g (Rectangle z w)
principalPart : EqOn (f - fun s => A / (s - p)) g (Rectangle z w \ {p})
principalPart' : EqOn f (g + fun s => A / (s - p)) (Rectangle z w \ {p})
this : EqOn f (g + fun s => A / (s - p)) (RectangleBorder z w)
t1 : RectangleBorderIntegrable g z w
x : ℂ
hx : x ∈ {p}ᶜ
⊢ x - p ≠ 0
Tactic:
rw [sub_ne_zero]
Proof state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f✝ g✝ : ℂ → E
z✝ w✝ p✝ c A✝ : ℂ
x✝ x₁ x₂ y y₁ y₂ σ : ℝ
f g : ℂ → ℂ
z w p A : ℂ
zRe_le_wRe : z.re ≤ w.re
zIm_le_wIm : z.im ≤ w.im
pInRectInterior : Rectangle z w ∈ 𝓝 p
gHolo : HolomorphicOn g (Rectangle z w)
principalPart : EqOn (f - fun s => A / (s - p)) g (Rectangle z w \ {p})
principalPart' : EqOn f (g + fun s => A / (s - p)) (Rectangle z w \ {p})
this : EqOn f (g + fun s => A / (s - p)) (RectangleBorder z w)
t1 : RectangleBorderIntegrable g z w
x : ℂ
hx : x ∈ {p}ᶜ
⊢ x ≠ p
Theorem: ResidueTheoremOnRectangleWithSimplePole
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f✝ g✝ : ℂ → E
z✝ w✝ p✝ c A✝ : ℂ
x✝ x₁ x₂ y y₁ y₂ σ : ℝ
f g : ℂ → ℂ
z w p A : ℂ
zRe_le_wRe : z.re ≤ w.re
zIm_le_wIm : z.im ≤ w.im
pInRectInterior : Rectangle z w ∈ 𝓝 p
gHolo : HolomorphicOn g (Rectangle z w)
principalPart : EqOn (f - fun s => A / (s - p)) g (Rectangle z w \ {p})
principalPart' : EqOn f (g + fun s => A / (s - p)) (Rectangle z w \ {p})
this : EqOn f (g + fun s => A / (s - p)) (RectangleBorder z w)
t1 : RectangleBorderIntegrable g z w
x : ℂ
hx : x ∈ {p}ᶜ
⊢ x ≠ p
Tactic:
exact hx
Proof state after:
no goals
Theorem: ResidueTheoremOnRectangleWithSimplePole
Proof state before:
case st
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f✝ g✝ : ℂ → E
z✝ w✝ p✝ c A✝ : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
f g : ℂ → ℂ
z w p A : ℂ
zRe_le_wRe : z.re ≤ w.re
zIm_le_wIm : z.im ≤ w.im
pInRectInterior : Rectangle z w ∈ 𝓝 p
gHolo : HolomorphicOn g (Rectangle z w)
principalPart : EqOn (f - fun s => A / (s - p)) g (Rectangle z w \ {p})
principalPart' : EqOn f (g + fun s => A / (s - p)) (Rectangle z w \ {p})
this : EqOn f (g + fun s => A / (s - p)) (RectangleBorder z w)
t1 : RectangleBorderIntegrable g z w
⊢ Rectangle z w \ {p} ⊆ {p}ᶜ
Tactic:
rintro s ⟨_, hs⟩
Proof state after:
case st.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f✝ g✝ : ℂ → E
z✝ w✝ p✝ c A✝ : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
f g : ℂ → ℂ
z w p A : ℂ
zRe_le_wRe : z.re ≤ w.re
zIm_le_wIm : z.im ≤ w.im
pInRectInterior : Rectangle z w ∈ 𝓝 p
gHolo : HolomorphicOn g (Rectangle z w)
principalPart : EqOn (f - fun s => A / (s - p)) g (Rectangle z w \ {p})
principalPart' : EqOn f (g + fun s => A / (s - p)) (Rectangle z w \ {p})
this : EqOn f (g + fun s => A / (s - p)) (RectangleBorder z w)
t1 : RectangleBorderIntegrable g z w
s : ℂ
left✝ : s ∈ Rectangle z w
hs : s ∉ {p}
⊢ s ∈ {p}ᶜ
Theorem: ResidueTheoremOnRectangleWithSimplePole
Proof state before:
case st.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f✝ g✝ : ℂ → E
z✝ w✝ p✝ c A✝ : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
f g : ℂ → ℂ
z w p A : ℂ
zRe_le_wRe : z.re ≤ w.re
zIm_le_wIm : z.im ≤ w.im
pInRectInterior : Rectangle z w ∈ 𝓝 p
gHolo : HolomorphicOn g (Rectangle z w)
principalPart : EqOn (f - fun s => A / (s - p)) g (Rectangle z w \ {p})
principalPart' : EqOn f (g + fun s => A / (s - p)) (Rectangle z w \ {p})
this : EqOn f (g + fun s => A / (s - p)) (RectangleBorder z w)
t1 : RectangleBorderIntegrable g z w
s : ℂ
left✝ : s ∈ Rectangle z w
hs : s ∉ {p}
⊢ s ∈ {p}ᶜ
Tactic:
exact hs
Proof state after:
no goals
Theorem: ResidueTheoremOnRectangleWithSimplePole
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f✝ g✝ : ℂ → E
z✝ w✝ p✝ c A✝ : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
f g : ℂ → ℂ
z w p A : ℂ
zRe_le_wRe : z.re ≤ w.re
zIm_le_wIm : z.im ≤ w.im
pInRectInterior : Rectangle z w ∈ 𝓝 p
gHolo : HolomorphicOn g (Rectangle z w)
principalPart : EqOn (f - fun s => A / (s - p)) g (Rectangle z w \ {p})
principalPart' : EqOn f (g + fun s => A / (s - p)) (Rectangle z w \ {p})
this : EqOn f (g + fun s => A / (s - p)) (RectangleBorder z w)
t1 : RectangleBorderIntegrable g z w
t2 : HolomorphicOn (fun s => A / (s - p)) (Rectangle z w \ {p})
t3 : RectangleBorderIntegrable (fun s => A / (s - p)) z w
⊢ Rectangle z w ⊆ Rectangle z w
Tactic:
rfl
Proof state after:
no goals
Theorem: MeasureTheory.LocallyIntegrable.integrable_of_isBigO_atTop_of_norm_eq_norm_neg
Proof state before:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : MeasurableSpace α
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
f : α → E
g : α → F
a b : α
μ : Measure α
l : Filter α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : CompactIccSpace α
inst✝² : atTop.IsMeasurablyGenerated
inst✝¹ : MeasurableNeg α
inst✝ : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
⊢ Integrable f μ
Tactic:
refine (isEmpty_or_nonempty α).casesOn (fun _ ↦ Integrable.of_finite μ f) (fun _ ↦ ?_)
Proof state after:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : MeasurableSpace α
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
f : α → E
g : α → F
a b : α
μ : Measure α
l : Filter α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : CompactIccSpace α
inst✝² : atTop.IsMeasurablyGenerated
inst✝¹ : MeasurableNeg α
inst✝ : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
x✝ : Nonempty α
⊢ Integrable f μ
Theorem: MeasureTheory.LocallyIntegrable.integrable_of_isBigO_atTop_of_norm_eq_norm_neg
Proof state before:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : MeasurableSpace α
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
f : α → E
g : α → F
a b : α
μ : Measure α
l : Filter α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : CompactIccSpace α
inst✝² : atTop.IsMeasurablyGenerated
inst✝¹ : MeasurableNeg α
inst✝ : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
x✝ : Nonempty α
⊢ Integrable f μ
Tactic:
let a := -|Classical.arbitrary α|
Proof state after:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : MeasurableSpace α
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
f : α → E
g : α → F
a✝ b : α
μ : Measure α
l : Filter α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : CompactIccSpace α
inst✝² : atTop.IsMeasurablyGenerated
inst✝¹ : MeasurableNeg α
inst✝ : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
x✝ : Nonempty α
a : α := -|Classical.arbitrary α|
⊢ Integrable f μ
Theorem: MeasureTheory.LocallyIntegrable.integrable_of_isBigO_atTop_of_norm_eq_norm_neg
Proof state before:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : MeasurableSpace α
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
f : α → E
g : α → F
a✝ b : α
μ : Measure α
l : Filter α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : CompactIccSpace α
inst✝² : atTop.IsMeasurablyGenerated
inst✝¹ : MeasurableNeg α
inst✝ : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
x✝ : Nonempty α
a : α := -|Classical.arbitrary α|
⊢ Integrable f μ
Tactic:
have h_int : IntegrableOn f (Ici a) μ :=
  LocallyIntegrableOn.integrableOn_of_isBigO_atTop (hf.locallyIntegrableOn _) ho hg
Proof state after:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : MeasurableSpace α
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
f : α → E
g : α → F
a✝ b : α
μ : Measure α
l : Filter α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : CompactIccSpace α
inst✝² : atTop.IsMeasurablyGenerated
inst✝¹ : MeasurableNeg α
inst✝ : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
x✝ : Nonempty α
a : α := -|Classical.arbitrary α|
h_int : IntegrableOn f (Ici a) μ
⊢ Integrable f μ
Theorem: MeasureTheory.LocallyIntegrable.integrable_of_isBigO_atTop_of_norm_eq_norm_neg
Proof state before:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : MeasurableSpace α
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
f : α → E
g : α → F
a✝ b : α
μ : Measure α
l : Filter α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : CompactIccSpace α
inst✝² : atTop.IsMeasurablyGenerated
inst✝¹ : MeasurableNeg α
inst✝ : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
x✝ : Nonempty α
a : α := -|Classical.arbitrary α|
h_int : IntegrableOn f (Ici a) μ
⊢ Integrable f μ
Tactic:
have h_map_neg : (μ.restrict (Ici a)).map Neg.neg = μ.restrict (Iic (-a)) := by
  rw [show Ici a = Neg.neg ⁻¹' Iic (-a) by simp, ← measurableEmbedding_neg.restrict_map,
    Measure.map_neg_eq_self]
Proof state after:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : MeasurableSpace α
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
f : α → E
g : α → F
a✝ b : α
μ : Measure α
l : Filter α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : CompactIccSpace α
inst✝² : atTop.IsMeasurablyGenerated
inst✝¹ : MeasurableNeg α
inst✝ : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
x✝ : Nonempty α
a : α := -|Classical.arbitrary α|
h_int : IntegrableOn f (Ici a) μ
h_map_neg : Measure.map Neg.neg (μ.restrict (Ici a)) = μ.restrict (Iic (-a))
⊢ Integrable f μ