Theorem: RectangleIntegralVSplit' (PrimeNumberTheoremAnd/ResidueCalcOnRectangles.lean)

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₂ σ b x₀ x₁ y₀ y₁ : ℝ
hb : b ∈ [[y₀, y₁]]
hf : RectangleBorderIntegrable f (↑x₀ + ↑y₀ * I) (↑x₁ + ↑y₁ * I)
⊢ IntervalIntegrable (fun y => f (↑x₀ + ↑y * I)) volume y₀ y₁
Tactic:
simpa using hf.2.2.2
State after:
no goals

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₂ σ b x₀ x₁ y₀ y₁ : ℝ
hb : b ∈ [[y₀, y₁]]
hf : RectangleBorderIntegrable f (↑x₀ + ↑y₀ * I) (↑x₁ + ↑y₁ * I)
⊢ IntervalIntegrable (fun y => f (↑x₁ + ↑y * I)) volume y₀ y₁
Tactic:
simpa using hf.2.2.1
State after:
no goals