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