AlexKontorovich/PrimeNumberTheoremAnd
Source indexedlemma · leanprover/lean4:v4.32.0
RectangleIntegralHSplit
PrimeNumberTheoremAnd.ResidueCalcOnRectangles · PrimeNumberTheoremAnd/ResidueCalcOnRectangles.lean:256 to 293
Source documentation
Given x₀ a x₁ : ℝ, and y₀ y₁ : ℝ and a function
f : ℂ → ℂ so that both (t : ℝ) ↦ f(t + y₀ * I) and
(t : ℝ) ↦ f(t + y₁ * I) are integrable over both
t ∈ Icc x₀ a and t ∈ Icc a x₁, we have that
RectangleIntegral f (x₀ + y₀ * I) (x₁ + y₁ * I) is the sum of
RectangleIntegral f (x₀ + y₀ * I) (a + y₁ * I) and
RectangleIntegral f (a + y₀ * I) (x₁ + y₁ * I).
Exact Lean statement
lemma RectangleIntegralHSplit {a x₀ x₁ y₀ y₁ : ℝ}
(f_int_x₀_a_bot : IntervalIntegrable (fun x => f (↑x + ↑y₀ * I)) volume x₀ a)
(f_int_a_x₁_bot : IntervalIntegrable (fun x => f (↑x + ↑y₀ * I)) volume a x₁)
(f_int_x₀_a_top : IntervalIntegrable (fun x => f (↑x + ↑y₁ * I)) volume x₀ a)
(f_int_a_x₁_top : IntervalIntegrable (fun x => f (↑x + ↑y₁ * I)) volume a x₁) :
RectangleIntegral f (x₀ + y₀ * I) (x₁ + y₁ * I) =
RectangleIntegral f (x₀ + y₀ * I) (a + y₁ * I) +
RectangleIntegral f (a + y₀ * I) (x₁ + y₁ * I)Complete declaration
Lean source
Full Lean sourceLean 4
lemma RectangleIntegralHSplit {a x₀ x₁ y₀ y₁ : ℝ} (f_int_x₀_a_bot : IntervalIntegrable (fun x => f (↑x + ↑y₀ * I)) volume x₀ a) (f_int_a_x₁_bot : IntervalIntegrable (fun x => f (↑x + ↑y₀ * I)) volume a x₁) (f_int_x₀_a_top : IntervalIntegrable (fun x => f (↑x + ↑y₁ * I)) volume x₀ a) (f_int_a_x₁_top : IntervalIntegrable (fun x => f (↑x + ↑y₁ * I)) volume a x₁) : RectangleIntegral f (x₀ + y₀ * I) (x₁ + y₁ * I) = RectangleIntegral f (x₀ + y₀ * I) (a + y₁ * I) + RectangleIntegral f (a + y₀ * 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_x₀_a_bot f_int_a_x₁_bot have h₂ := integral_add_adjacent_intervals f_int_x₀_a_top f_int_a_x₁_top have h₁' : (∫ (x : ℝ) in x₀..a, f (↑x + ↑y₀ * I)) + ∫ (x : ℝ) in a..x₁, f (↑y₀ * I + ↑x) = ∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₀ * I) := by simpa [add_comm] using h₁ have h₂' : (∫ (x : ℝ) in x₀..a, f (↑x + ↑y₁ * I)) + ∫ (x : ℝ) in a..x₁, f (↑y₁ * I + ↑x) = ∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₁ * I) := by simpa [add_comm] using h₂ rw [← h₁', ← h₂'] have hcomm₁ : ∫ (x : ℝ) in a..x₁, f (↑y₀ * I + ↑x) = ∫ (x : ℝ) in a..x₁, f (↑x + ↑y₀ * I) := by apply intervalIntegral.integral_congr intro x _ exact congrArg f (by ring) have hcomm₂ : ∫ (x : ℝ) in a..x₁, f (↑y₁ * I + ↑x) = ∫ (x : ℝ) in a..x₁, f (↑x + ↑y₁ * I) := by apply intervalIntegral.integral_congr intro x _ exact congrArg f (by ring) rw [hcomm₁, hcomm₂] abel