Source indexedtheorem · leanprover/lean4:v4.32.0

rectangleIntegral'_eq12

PrimeNumberTheoremAnd.IEANTN.KadiriEq12Helpers · PrimeNumberTheoremAnd/IEANTN/KadiriEq12Helpers.lean:358 to 376

Source documentation

Side identification: the rectangle integral of f over the box [-a,1+a]×[-T,T] splits into the two vertical and two horizontal pieces appearing in eq. (12).

Exact Lean statement

theorem rectangleIntegral'_eq12 (f : ℂ → ℂ) {a T : ℝ} (hTT : -T ≤ T) (ha : -a ≤ 1 + a) :
    RectangleIntegral' f ((-a : ℝ) - T * I) ((1 + a : ℝ) + T * I)
      = (1 / (2 * (Real.pi : ℂ))) * (∫ t in Ioo (-T) T, f ((1 + a : ℝ) + t * I))
        - (1 / (2 * (Real.pi : ℂ))) * (∫ t in Ioo (-T) T, f ((-a : ℝ) + t * I))
        - (1 / (2 * (Real.pi : ℂ) * I)) * (∫ σ in Ioo (-a) (1 + a), f ((σ : ℝ) + T * I))
        + (1 / (2 * (Real.pi : ℂ) * I)) * (∫ σ in Ioo (-a) (1 + a), f ((σ : ℝ) + (-T : ℝ) * I))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem rectangleIntegral'_eq12 (f : ℂ → ℂ) {a T : ℝ} (hTT : -T ≤ T) (ha : -a ≤ 1 + a) :    RectangleIntegral' f ((-a : ℝ) - T * I) ((1 + a : ℝ) + T * I)      = (1 / (2 * (Real.pi : ℂ))) * (∫ t in Ioo (-T) T, f ((1 + a : ℝ) + t * I))        - (1 / (2 * (Real.pi : ℂ))) * (∫ t in Ioo (-T) T, f ((-a : ℝ) + t * I))        - (1 / (2 * (Real.pi : ℂ) * I)) * (∫ σ in Ioo (-a) (1 + a), f ((σ : ℝ) + T * I))        + (1 / (2 * (Real.pi : ℂ) * I)) * (∫ σ in Ioo (-a) (1 + a), f ((σ : ℝ) + (-T : ℝ) * I)) := by  have hzre : ((-a : ℝ) - (T : ℂ) * I).re = -a := by simp  have hzim : ((-a : ℝ) - (T : ℂ) * I).im = -T := by simp  have hwre : ((1 + a : ℝ) + (T : ℂ) * I).re = 1 + a := by simp  have hwim : ((1 + a : ℝ) + (T : ℂ) * I).im = T := by simp  unfold RectangleIntegral' RectangleIntegral HIntegral VIntegral  rw [hzre, hzim, hwre, hwim]  rw [intervalIntegral.integral_of_le ha, intervalIntegral.integral_of_le ha,      intervalIntegral.integral_of_le hTT, intervalIntegral.integral_of_le hTT]  rw [integral_Ioc_eq_integral_Ioo, integral_Ioc_eq_integral_Ioo,      integral_Ioc_eq_integral_Ioo, integral_Ioc_eq_integral_Ioo]  simp only [smul_eq_mul]  field_simp  ring