Source indexedlemma · leanprover/lean4:v4.32.0

RectangleIntegralVSplit

PrimeNumberTheoremAnd.ResidueCalcOnRectangles · PrimeNumberTheoremAnd/ResidueCalcOnRectangles.lean:307 to 321

Mathematical statement

Exact Lean statement

lemma RectangleIntegralVSplit {b x₀ x₁ y₀ y₁ : ℝ}
    (f_int_y₀_b_left : IntervalIntegrable (fun y => f (x₀ + y * I)) volume y₀ b)
    (f_int_b_y₁_left : IntervalIntegrable (fun y => f (x₀ + y * I)) volume b y₁)
    (f_int_y₀_b_right : IntervalIntegrable (fun y => f (x₁ + y * I)) volume y₀ b)
    (f_int_b_y₁_right : IntervalIntegrable (fun y => f (x₁ + y * I)) volume b y₁) :
    RectangleIntegral f (x₀ + y₀ * I) (x₁ + y₁ * I) =
      RectangleIntegral f (x₀ + y₀ * I) (x₁ + b * I) +
      RectangleIntegral f (x₀ + b * I) (x₁ + y₁ * I)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma RectangleIntegralVSplit {b x₀ x₁ y₀ y₁ : ℝ}    (f_int_y₀_b_left : IntervalIntegrable (fun y => f (x₀ + y * I)) volume y₀ b)    (f_int_b_y₁_left : IntervalIntegrable (fun y => f (x₀ + y * I)) volume b y₁)    (f_int_y₀_b_right : IntervalIntegrable (fun y => f (x₁ + y * I)) volume y₀ b)    (f_int_b_y₁_right : IntervalIntegrable (fun y => f (x₁ + y * I)) volume b y₁) :    RectangleIntegral f (x₀ + y₀ * I) (x₁ + y₁ * I) =      RectangleIntegral f (x₀ + y₀ * I) (x₁ + b * I) +      RectangleIntegral f (x₀ + b * I) (x₁ + y₁ * I) := by  dsimp [RectangleIntegral, HIntegral, VIntegral]  simp only [Complex.mul_re, Complex.mul_im, Complex.ofReal_re, Complex.ofReal_im, Complex.I_re,    Complex.I_im, mul_one, mul_zero, add_zero, zero_add, sub_self]  have h₁ := integral_add_adjacent_intervals f_int_y₀_b_left f_int_b_y₁_left  have h₂ := integral_add_adjacent_intervals f_int_y₀_b_right f_int_b_y₁_right  rw [← h₁, ← h₂]  module