Theorem: DiffVertRect_eq_UpperLowerUs (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₂ σ✝ σ σ' T : ℝ
f_int_σ : Integrable (fun t => f (↑σ + ↑t * I)) volume
f_int_σ' : Integrable (fun t => f (↑σ' + ↑t * I)) volume
⊢ VerticalIntegral f σ' - VerticalIntegral f σ - RectangleIntegral f (↑σ - I * ↑T) (↑σ' + I * ↑T) =
    UpperUIntegral f σ σ' T - LowerUIntegral f σ σ' T
Tactic:
rw [verticalIntegral_split_three (-T) T f_int_σ, verticalIntegral_split_three (-T) T f_int_σ']
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₂ σ✝ σ σ' T : ℝ
f_int_σ : Integrable (fun t => f (↑σ + ↑t * I)) volume
f_int_σ' : Integrable (fun t => f (↑σ' + ↑t * I)) volume
⊢ ((I • ∫ (t : ℝ) in Iic (-T), f (↑σ' + ↑t * I)) + VIntegral f σ' (-T) T + I • ∫ (t : ℝ) in Ici T, f (↑σ' + ↑t * I)) -
        ((I • ∫ (t : ℝ) in Iic (-T), f (↑σ + ↑t * I)) + VIntegral f σ (-T) T +
          I • ∫ (t : ℝ) in Ici T, f (↑σ + ↑t * I)) -
      RectangleIntegral f (↑σ - I * ↑T) (↑σ' + I * ↑T) =
    UpperUIntegral f σ σ' T - LowerUIntegral f σ σ' T

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₂ σ✝ σ σ' T : ℝ
f_int_σ : Integrable (fun t => f (↑σ + ↑t * I)) volume
f_int_σ' : Integrable (fun t => f (↑σ' + ↑t * I)) volume
⊢ ((I • ∫ (t : ℝ) in Iic (-T), f (↑σ' + ↑t * I)) + VIntegral f σ' (-T) T + I • ∫ (t : ℝ) in Ici T, f (↑σ' + ↑t * I)) -
        ((I • ∫ (t : ℝ) in Iic (-T), f (↑σ + ↑t * I)) + VIntegral f σ (-T) T +
          I • ∫ (t : ℝ) in Ici T, f (↑σ + ↑t * I)) -
      RectangleIntegral f (↑σ - I * ↑T) (↑σ' + I * ↑T) =
    UpperUIntegral f σ σ' T - LowerUIntegral f σ σ' T
Tactic:
simp only [RectangleIntegral, UpperUIntegral, LowerUIntegral]
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₂ σ✝ σ σ' T : ℝ
f_int_σ : Integrable (fun t => f (↑σ + ↑t * I)) volume
f_int_σ' : Integrable (fun t => f (↑σ' + ↑t * I)) volume
⊢ ((I • ∫ (t : ℝ) in Iic (-T), f (↑σ' + ↑t * I)) + VIntegral f σ' (-T) T + I • ∫ (t : ℝ) in Ici T, f (↑σ' + ↑t * I)) -
        ((I • ∫ (t : ℝ) in Iic (-T), f (↑σ + ↑t * I)) + VIntegral f σ (-T) T +
          I • ∫ (t : ℝ) in Ici T, f (↑σ + ↑t * I)) -
      (HIntegral f (↑σ - I * ↑T).re (↑σ' + I * ↑T).re (↑σ - I * ↑T).im -
            HIntegral f (↑σ - I * ↑T).re (↑σ' + I * ↑T).re (↑σ' + I * ↑T).im +
          VIntegral f (↑σ' + I * ↑T).re (↑σ - I * ↑T).im (↑σ' + I * ↑T).im -
        VIntegral f (↑σ - I * ↑T).re (↑σ - I * ↑T).im (↑σ' + I * ↑T).im) =
    ((HIntegral f σ σ' T + I • ∫ (t : ℝ) in Ici T, f (↑σ' + ↑t * I)) - I • ∫ (t : ℝ) in Ici T, f (↑σ + ↑t * I)) -
      ((HIntegral f σ σ' (-T) - I • ∫ (t : ℝ) in Iic (-T), f (↑σ' + ↑t * I)) +
        I • ∫ (t : ℝ) in Iic (-T), f (↑σ + ↑t * 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₂ σ✝ σ σ' T : ℝ
f_int_σ : Integrable (fun t => f (↑σ + ↑t * I)) volume
f_int_σ' : Integrable (fun t => f (↑σ' + ↑t * I)) volume
⊢ ((I • ∫ (t : ℝ) in Iic (-T), f (↑σ' + ↑t * I)) + VIntegral f σ' (-T) T + I • ∫ (t : ℝ) in Ici T, f (↑σ' + ↑t * I)) -
        ((I • ∫ (t : ℝ) in Iic (-T), f (↑σ + ↑t * I)) + VIntegral f σ (-T) T +
          I • ∫ (t : ℝ) in Ici T, f (↑σ + ↑t * I)) -
      (HIntegral f (↑σ - I * ↑T).re (↑σ' + I * ↑T).re (↑σ - I * ↑T).im -
            HIntegral f (↑σ - I * ↑T).re (↑σ' + I * ↑T).re (↑σ' + I * ↑T).im +
          VIntegral f (↑σ' + I * ↑T).re (↑σ - I * ↑T).im (↑σ' + I * ↑T).im -
        VIntegral f (↑σ - I * ↑T).re (↑σ - I * ↑T).im (↑σ' + I * ↑T).im) =
    ((HIntegral f σ σ' T + I • ∫ (t : ℝ) in Ici T, f (↑σ' + ↑t * I)) - I • ∫ (t : ℝ) in Ici T, f (↑σ + ↑t * I)) -
      ((HIntegral f σ σ' (-T) - I • ∫ (t : ℝ) in Iic (-T), f (↑σ' + ↑t * I)) +
        I • ∫ (t : ℝ) in Iic (-T), f (↑σ + ↑t * I))
Tactic:
simp only [sub_re, mul_re, I_re, add_re, ofReal_re, I_im, ofReal_im, sub_im, mul_im, add_im]
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₂ σ✝ σ σ' T : ℝ
f_int_σ : Integrable (fun t => f (↑σ + ↑t * I)) volume
f_int_σ' : Integrable (fun t => f (↑σ' + ↑t * I)) volume
⊢ ((I • ∫ (t : ℝ) in Iic (-T), f (↑σ' + ↑t * I)) + VIntegral f σ' (-T) T + I • ∫ (t : ℝ) in Ici T, f (↑σ' + ↑t * I)) -
        ((I • ∫ (t : ℝ) in Iic (-T), f (↑σ + ↑t * I)) + VIntegral f σ (-T) T +
          I • ∫ (t : ℝ) in Ici T, f (↑σ + ↑t * I)) -
      (HIntegral f (σ - (0 * T - 1 * 0)) (σ' + (0 * T - 1 * 0)) (0 - (0 * 0 + 1 * T)) -
            HIntegral f (σ - (0 * T - 1 * 0)) (σ' + (0 * T - 1 * 0)) (0 + (0 * 0 + 1 * T)) +
          VIntegral f (σ' + (0 * T - 1 * 0)) (0 - (0 * 0 + 1 * T)) (0 + (0 * 0 + 1 * T)) -
        VIntegral f (σ - (0 * T - 1 * 0)) (0 - (0 * 0 + 1 * T)) (0 + (0 * 0 + 1 * T))) =
    ((HIntegral f σ σ' T + I • ∫ (t : ℝ) in Ici T, f (↑σ' + ↑t * I)) - I • ∫ (t : ℝ) in Ici T, f (↑σ + ↑t * I)) -
      ((HIntegral f σ σ' (-T) - I • ∫ (t : ℝ) in Iic (-T), f (↑σ' + ↑t * I)) +
        I • ∫ (t : ℝ) in Iic (-T), f (↑σ + ↑t * 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₂ σ✝ σ σ' T : ℝ
f_int_σ : Integrable (fun t => f (↑σ + ↑t * I)) volume
f_int_σ' : Integrable (fun t => f (↑σ' + ↑t * I)) volume
⊢ ((I • ∫ (t : ℝ) in Iic (-T), f (↑σ' + ↑t * I)) + VIntegral f σ' (-T) T + I • ∫ (t : ℝ) in Ici T, f (↑σ' + ↑t * I)) -
        ((I • ∫ (t : ℝ) in Iic (-T), f (↑σ + ↑t * I)) + VIntegral f σ (-T) T +
          I • ∫ (t : ℝ) in Ici T, f (↑σ + ↑t * I)) -
      (HIntegral f (σ - (0 * T - 1 * 0)) (σ' + (0 * T - 1 * 0)) (0 - (0 * 0 + 1 * T)) -
            HIntegral f (σ - (0 * T - 1 * 0)) (σ' + (0 * T - 1 * 0)) (0 + (0 * 0 + 1 * T)) +
          VIntegral f (σ' + (0 * T - 1 * 0)) (0 - (0 * 0 + 1 * T)) (0 + (0 * 0 + 1 * T)) -
        VIntegral f (σ - (0 * T - 1 * 0)) (0 - (0 * 0 + 1 * T)) (0 + (0 * 0 + 1 * T))) =
    ((HIntegral f σ σ' T + I • ∫ (t : ℝ) in Ici T, f (↑σ' + ↑t * I)) - I • ∫ (t : ℝ) in Ici T, f (↑σ + ↑t * I)) -
      ((HIntegral f σ σ' (-T) - I • ∫ (t : ℝ) in Iic (-T), f (↑σ' + ↑t * I)) +
        I • ∫ (t : ℝ) in Iic (-T), f (↑σ + ↑t * 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₂ σ✝ σ σ' T : ℝ
f_int_σ : Integrable (fun t => f (↑σ + ↑t * I)) volume
f_int_σ' : Integrable (fun t => f (↑σ' + ↑t * I)) volume
⊢ ((I • ∫ (t : ℝ) in Iic (-T), f (↑σ' + ↑t * I)) + VIntegral f σ' (-T) T + I • ∫ (t : ℝ) in Ici T, f (↑σ' + ↑t * I)) -
        ((I • ∫ (t : ℝ) in Iic (-T), f (↑σ + ↑t * I)) + VIntegral f σ (-T) T +
          I • ∫ (t : ℝ) in Ici T, f (↑σ + ↑t * I)) -
      (HIntegral f σ σ' (-T) - HIntegral f σ σ' T + VIntegral f σ' (-T) T - VIntegral f σ (-T) T) =
    ((HIntegral f σ σ' T + I • ∫ (t : ℝ) in Ici T, f (↑σ' + ↑t * I)) - I • ∫ (t : ℝ) in Ici T, f (↑σ + ↑t * I)) -
      ((HIntegral f σ σ' (-T) - I • ∫ (t : ℝ) in Iic (-T), f (↑σ' + ↑t * I)) +
        I • ∫ (t : ℝ) in Iic (-T), f (↑σ + ↑t * 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₂ σ✝ σ σ' T : ℝ
f_int_σ : Integrable (fun t => f (↑σ + ↑t * I)) volume
f_int_σ' : Integrable (fun t => f (↑σ' + ↑t * I)) volume
⊢ ((I • ∫ (t : ℝ) in Iic (-T), f (↑σ' + ↑t * I)) + VIntegral f σ' (-T) T + I • ∫ (t : ℝ) in Ici T, f (↑σ' + ↑t * I)) -
        ((I • ∫ (t : ℝ) in Iic (-T), f (↑σ + ↑t * I)) + VIntegral f σ (-T) T +
          I • ∫ (t : ℝ) in Ici T, f (↑σ + ↑t * I)) -
      (HIntegral f σ σ' (-T) - HIntegral f σ σ' T + VIntegral f σ' (-T) T - VIntegral f σ (-T) T) =
    ((HIntegral f σ σ' T + I • ∫ (t : ℝ) in Ici T, f (↑σ' + ↑t * I)) - I • ∫ (t : ℝ) in Ici T, f (↑σ + ↑t * I)) -
      ((HIntegral f σ σ' (-T) - I • ∫ (t : ℝ) in Iic (-T), f (↑σ' + ↑t * I)) +
        I • ∫ (t : ℝ) in Iic (-T), f (↑σ + ↑t * I))
Tactic:
abel
State after:
no goals