Source indexedtheorem · leanprover/lean4:v4.32.0

RectangleBorderIntegrable.add

PrimeNumberTheoremAnd.ResidueCalcOnRectangles · PrimeNumberTheoremAnd/ResidueCalcOnRectangles.lean:210 to 219

Mathematical statement

Exact Lean statement

theorem RectangleBorderIntegrable.add {f g : ℂ → E}
    (hf : RectangleBorderIntegrable f z w) (hg : RectangleBorderIntegrable g z w) :
    RectangleIntegral (f + g) z w = RectangleIntegral f z w + RectangleIntegral g z w

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem RectangleBorderIntegrable.add {f g : ℂ → E}    (hf : RectangleBorderIntegrable f z w) (hg : RectangleBorderIntegrable g z w) :    RectangleIntegral (f + g) z w = RectangleIntegral f z w + RectangleIntegral g z w := by  dsimp [RectangleIntegral, HIntegral, VIntegral]  have h₁ := intervalIntegral.integral_add hf.1 hg.1  have h₂ := intervalIntegral.integral_add hf.2.1 hg.2.1  have h₃ := intervalIntegral.integral_add hf.2.2.1 hg.2.2.1  have h₄ := intervalIntegral.integral_add hf.2.2.2 hg.2.2.2  rw [h₁, h₂, h₃, h₄]  module