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₁ : ℝ
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)
Tactic:
dsimp [RectangleIntegral, HIntegral, VIntegral]
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₂ σ 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₁
⊢ (((∫ (x : ℝ) in x₀ + (y₀ * 0 - 0 * 1)..x₁ + (y₁ * 0 - 0 * 1), f (↑x + ↑(0 + (y₀ * 1 + 0 * 0)) * I)) -
          ∫ (x : ℝ) in x₀ + (y₀ * 0 - 0 * 1)..x₁ + (y₁ * 0 - 0 * 1), f (↑x + ↑(0 + (y₁ * 1 + 0 * 0)) * I)) +
        I • ∫ (y : ℝ) in 0 + (y₀ * 1 + 0 * 0)..0 + (y₁ * 1 + 0 * 0), f (↑(x₁ + (y₁ * 0 - 0 * 1)) + ↑y * I)) -
      I • ∫ (y : ℝ) in 0 + (y₀ * 1 + 0 * 0)..0 + (y₁ * 1 + 0 * 0), f (↑(x₀ + (y₀ * 0 - 0 * 1)) + ↑y * I) =
    ((((∫ (x : ℝ) in x₀ + (y₀ * 0 - 0 * 1)..x₁ + (b * 0 - 0 * 1), f (↑x + ↑(0 + (y₀ * 1 + 0 * 0)) * I)) -
            ∫ (x : ℝ) in x₀ + (y₀ * 0 - 0 * 1)..x₁ + (b * 0 - 0 * 1), f (↑x + ↑(0 + (b * 1 + 0 * 0)) * I)) +
          I • ∫ (y : ℝ) in 0 + (y₀ * 1 + 0 * 0)..0 + (b * 1 + 0 * 0), f (↑(x₁ + (b * 0 - 0 * 1)) + ↑y * I)) -
        I • ∫ (y : ℝ) in 0 + (y₀ * 1 + 0 * 0)..0 + (b * 1 + 0 * 0), f (↑(x₀ + (y₀ * 0 - 0 * 1)) + ↑y * I)) +
      ((((∫ (x : ℝ) in x₀ + (b * 0 - 0 * 1)..x₁ + (y₁ * 0 - 0 * 1), f (↑x + ↑(0 + (b * 1 + 0 * 0)) * I)) -
            ∫ (x : ℝ) in x₀ + (b * 0 - 0 * 1)..x₁ + (y₁ * 0 - 0 * 1), f (↑x + ↑(0 + (y₁ * 1 + 0 * 0)) * I)) +
          I • ∫ (y : ℝ) in 0 + (b * 1 + 0 * 0)..0 + (y₁ * 1 + 0 * 0), f (↑(x₁ + (y₁ * 0 - 0 * 1)) + ↑y * I)) -
        I • ∫ (y : ℝ) in 0 + (b * 1 + 0 * 0)..0 + (y₁ * 1 + 0 * 0), f (↑(x₀ + (b * 0 - 0 * 1)) + ↑y * I))

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₁ : ℝ
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₁
⊢ (((∫ (x : ℝ) in x₀ + (y₀ * 0 - 0 * 1)..x₁ + (y₁ * 0 - 0 * 1), f (↑x + ↑(0 + (y₀ * 1 + 0 * 0)) * I)) -
          ∫ (x : ℝ) in x₀ + (y₀ * 0 - 0 * 1)..x₁ + (y₁ * 0 - 0 * 1), f (↑x + ↑(0 + (y₁ * 1 + 0 * 0)) * I)) +
        I • ∫ (y : ℝ) in 0 + (y₀ * 1 + 0 * 0)..0 + (y₁ * 1 + 0 * 0), f (↑(x₁ + (y₁ * 0 - 0 * 1)) + ↑y * I)) -
      I • ∫ (y : ℝ) in 0 + (y₀ * 1 + 0 * 0)..0 + (y₁ * 1 + 0 * 0), f (↑(x₀ + (y₀ * 0 - 0 * 1)) + ↑y * I) =
    ((((∫ (x : ℝ) in x₀ + (y₀ * 0 - 0 * 1)..x₁ + (b * 0 - 0 * 1), f (↑x + ↑(0 + (y₀ * 1 + 0 * 0)) * I)) -
            ∫ (x : ℝ) in x₀ + (y₀ * 0 - 0 * 1)..x₁ + (b * 0 - 0 * 1), f (↑x + ↑(0 + (b * 1 + 0 * 0)) * I)) +
          I • ∫ (y : ℝ) in 0 + (y₀ * 1 + 0 * 0)..0 + (b * 1 + 0 * 0), f (↑(x₁ + (b * 0 - 0 * 1)) + ↑y * I)) -
        I • ∫ (y : ℝ) in 0 + (y₀ * 1 + 0 * 0)..0 + (b * 1 + 0 * 0), f (↑(x₀ + (y₀ * 0 - 0 * 1)) + ↑y * I)) +
      ((((∫ (x : ℝ) in x₀ + (b * 0 - 0 * 1)..x₁ + (y₁ * 0 - 0 * 1), f (↑x + ↑(0 + (b * 1 + 0 * 0)) * I)) -
            ∫ (x : ℝ) in x₀ + (b * 0 - 0 * 1)..x₁ + (y₁ * 0 - 0 * 1), f (↑x + ↑(0 + (y₁ * 1 + 0 * 0)) * I)) +
          I • ∫ (y : ℝ) in 0 + (b * 1 + 0 * 0)..0 + (y₁ * 1 + 0 * 0), f (↑(x₁ + (y₁ * 0 - 0 * 1)) + ↑y * I)) -
        I • ∫ (y : ℝ) in 0 + (b * 1 + 0 * 0)..0 + (y₁ * 1 + 0 * 0), f (↑(x₀ + (b * 0 - 0 * 1)) + ↑y * I))
Tactic:
ring_nf
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₂ σ 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₁
⊢ (((∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₀ * I)) - ∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₁ * I)) +
        I • ∫ (y : ℝ) in y₀..y₁, f (↑x₁ + ↑y * I)) -
      I • ∫ (y : ℝ) in y₀..y₁, f (↑x₀ + ↑y * I) =
    ((((∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₀ * I)) - ∫ (x : ℝ) in x₀..x₁, f (↑x + ↑b * I)) +
          I • ∫ (y : ℝ) in y₀..b, f (↑x₁ + ↑y * I)) -
        I • ∫ (y : ℝ) in y₀..b, f (↑x₀ + ↑y * I)) +
      ((((∫ (x : ℝ) in x₀..x₁, f (↑x + ↑b * I)) - ∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₁ * I)) +
          I • ∫ (y : ℝ) in b..y₁, f (↑x₁ + ↑y * I)) -
        I • ∫ (y : ℝ) in b..y₁, f (↑x₀ + ↑y * I))

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₁ : ℝ
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₁
⊢ (((∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₀ * I)) - ∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₁ * I)) +
        I • ∫ (y : ℝ) in y₀..y₁, f (↑x₁ + ↑y * I)) -
      I • ∫ (y : ℝ) in y₀..y₁, f (↑x₀ + ↑y * I) =
    ((((∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₀ * I)) - ∫ (x : ℝ) in x₀..x₁, f (↑x + ↑b * I)) +
          I • ∫ (y : ℝ) in y₀..b, f (↑x₁ + ↑y * I)) -
        I • ∫ (y : ℝ) in y₀..b, f (↑x₀ + ↑y * I)) +
      ((((∫ (x : ℝ) in x₀..x₁, f (↑x + ↑b * I)) - ∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₁ * I)) +
          I • ∫ (y : ℝ) in b..y₁, f (↑x₁ + ↑y * I)) -
        I • ∫ (y : ℝ) in b..y₁, f (↑x₀ + ↑y * I))
Tactic:
have h₁ := intervalIntegral.integral_add_adjacent_intervals f_int_y₀_b_left f_int_b_y₁_left
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₂ σ 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₁
h₁ :
  (∫ (x : ℝ) in y₀..b, f (↑x₀ + ↑x * I)) + ∫ (x : ℝ) in b..y₁, f (↑x₀ + ↑x * I) = ∫ (x : ℝ) in y₀..y₁, f (↑x₀ + ↑x * I)
⊢ (((∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₀ * I)) - ∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₁ * I)) +
        I • ∫ (y : ℝ) in y₀..y₁, f (↑x₁ + ↑y * I)) -
      I • ∫ (y : ℝ) in y₀..y₁, f (↑x₀ + ↑y * I) =
    ((((∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₀ * I)) - ∫ (x : ℝ) in x₀..x₁, f (↑x + ↑b * I)) +
          I • ∫ (y : ℝ) in y₀..b, f (↑x₁ + ↑y * I)) -
        I • ∫ (y : ℝ) in y₀..b, f (↑x₀ + ↑y * I)) +
      ((((∫ (x : ℝ) in x₀..x₁, f (↑x + ↑b * I)) - ∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₁ * I)) +
          I • ∫ (y : ℝ) in b..y₁, f (↑x₁ + ↑y * I)) -
        I • ∫ (y : ℝ) in b..y₁, f (↑x₀ + ↑y * I))

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₁ : ℝ
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₁
h₁ :
  (∫ (x : ℝ) in y₀..b, f (↑x₀ + ↑x * I)) + ∫ (x : ℝ) in b..y₁, f (↑x₀ + ↑x * I) = ∫ (x : ℝ) in y₀..y₁, f (↑x₀ + ↑x * I)
⊢ (((∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₀ * I)) - ∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₁ * I)) +
        I • ∫ (y : ℝ) in y₀..y₁, f (↑x₁ + ↑y * I)) -
      I • ∫ (y : ℝ) in y₀..y₁, f (↑x₀ + ↑y * I) =
    ((((∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₀ * I)) - ∫ (x : ℝ) in x₀..x₁, f (↑x + ↑b * I)) +
          I • ∫ (y : ℝ) in y₀..b, f (↑x₁ + ↑y * I)) -
        I • ∫ (y : ℝ) in y₀..b, f (↑x₀ + ↑y * I)) +
      ((((∫ (x : ℝ) in x₀..x₁, f (↑x + ↑b * I)) - ∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₁ * I)) +
          I • ∫ (y : ℝ) in b..y₁, f (↑x₁ + ↑y * I)) -
        I • ∫ (y : ℝ) in b..y₁, f (↑x₀ + ↑y * I))
Tactic:
have h₂ := intervalIntegral.integral_add_adjacent_intervals f_int_y₀_b_right f_int_b_y₁_right
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₂ σ 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₁
h₁ :
  (∫ (x : ℝ) in y₀..b, f (↑x₀ + ↑x * I)) + ∫ (x : ℝ) in b..y₁, f (↑x₀ + ↑x * I) = ∫ (x : ℝ) in y₀..y₁, f (↑x₀ + ↑x * I)
h₂ :
  (∫ (x : ℝ) in y₀..b, f (↑x₁ + ↑x * I)) + ∫ (x : ℝ) in b..y₁, f (↑x₁ + ↑x * I) = ∫ (x : ℝ) in y₀..y₁, f (↑x₁ + ↑x * I)
⊢ (((∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₀ * I)) - ∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₁ * I)) +
        I • ∫ (y : ℝ) in y₀..y₁, f (↑x₁ + ↑y * I)) -
      I • ∫ (y : ℝ) in y₀..y₁, f (↑x₀ + ↑y * I) =
    ((((∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₀ * I)) - ∫ (x : ℝ) in x₀..x₁, f (↑x + ↑b * I)) +
          I • ∫ (y : ℝ) in y₀..b, f (↑x₁ + ↑y * I)) -
        I • ∫ (y : ℝ) in y₀..b, f (↑x₀ + ↑y * I)) +
      ((((∫ (x : ℝ) in x₀..x₁, f (↑x + ↑b * I)) - ∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₁ * I)) +
          I • ∫ (y : ℝ) in b..y₁, f (↑x₁ + ↑y * I)) -
        I • ∫ (y : ℝ) in b..y₁, f (↑x₀ + ↑y * I))

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₁ : ℝ
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₁
h₁ :
  (∫ (x : ℝ) in y₀..b, f (↑x₀ + ↑x * I)) + ∫ (x : ℝ) in b..y₁, f (↑x₀ + ↑x * I) = ∫ (x : ℝ) in y₀..y₁, f (↑x₀ + ↑x * I)
h₂ :
  (∫ (x : ℝ) in y₀..b, f (↑x₁ + ↑x * I)) + ∫ (x : ℝ) in b..y₁, f (↑x₁ + ↑x * I) = ∫ (x : ℝ) in y₀..y₁, f (↑x₁ + ↑x * I)
⊢ (((∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₀ * I)) - ∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₁ * I)) +
        I • ∫ (y : ℝ) in y₀..y₁, f (↑x₁ + ↑y * I)) -
      I • ∫ (y : ℝ) in y₀..y₁, f (↑x₀ + ↑y * I) =
    ((((∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₀ * I)) - ∫ (x : ℝ) in x₀..x₁, f (↑x + ↑b * I)) +
          I • ∫ (y : ℝ) in y₀..b, f (↑x₁ + ↑y * I)) -
        I • ∫ (y : ℝ) in y₀..b, f (↑x₀ + ↑y * I)) +
      ((((∫ (x : ℝ) in x₀..x₁, f (↑x + ↑b * I)) - ∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₁ * I)) +
          I • ∫ (y : ℝ) in b..y₁, f (↑x₁ + ↑y * I)) -
        I • ∫ (y : ℝ) in b..y₁, f (↑x₀ + ↑y * I))
Tactic:
additive_combination I • h₁ - I • h₂
State after:
no goals