Project-declaredLean 4.32.0 · mathlib@81a5d257c8e4

Rectangle Integral HSplit

RectangleIntegralHSplit

analytic number theory prime numbers asymptotics residue calc on rectangles

Plain-language statement

A vertical splitting identity for rectangular contour integrals. Under integrability of $f$ along the two horizontal sides, splitting the rectangle with real coordinates from $x_0$ to $x_1$ at $a$ gives $\int_{\partial R(x_0,x_1;y_0,y_1)}f=\int_{\partial R(x_0,a;y_0,y_1)}f+\int_{\partial R(a,x_1;y_0,y_1)}f.$ The two integrals over the shared vertical side cancel.

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)

Formal artifact

Lean source

Canonical 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

Project: Prime Number Theorem and More
License: Apache-2.0
Commit: a93551347dce
Source: PrimeNumberTheoremAnd/ResidueCalcOnRectangles.lean:256-293

Reuse this declaration

Bring the exact result into your workflow

The import identifies the source module. Your project still needs the pinned package dependency shown on this page.

What this badge means

This completion status comes from the project or community source. It has not yet been represented here as an independent rebuild and axiom audit.

Continue in this project

Related declarations

Project-declaredLean 4.32.0

Admissible bound mono

admissible_bound.mono

Plain-language statement

For positive parameters $A,B,C,R$ , the classical error-bound function $A\left(\frac{\log x}{R}\right)^B\exp\!\left(-C\sqrt{\frac{\log x}{R}}\right)$ is nonincreasing once $x\ge \exp\!\left(R(2B/C)^2\right)$ .

analytic number theoryprime numbersasymptotics

Source project: Prime Number Theorem and More

Person-level attribution pending.

View proof record

Project-declaredLean 4.32.0

Analytic On div Removable zero

AnalyticOn_divRemovable_zero

Plain-language statement

Let $f$ be analytic on an open set $s$ containing $0$ , and suppose $f(0)=0$ . Define $g(z)=f(z)/z$ for $z\ne0$ and $g(0)=f'(0)$ . Then the apparent singularity at $0$ is removable and $g$ is analytic throughout $s$ .

analytic number theoryprime numbersasymptotics

Source project: Prime Number Theorem and More

Person-level attribution pending.

View proof record

Project-declaredLean 4.32.0

Analytic On div Removable zero closed Ball

AnalyticOn_divRemovable_zero_closedBall

Plain-language statement

Suppose $R>0$ and $f$ is analytic on the closed disc $|z|\le R$ with $f(0)=0$ . Define $g(z)=f(z)/z$ for $z\ne0$ and $g(0)=f'(0)$ . Then $g$ is analytic on the entire closed disc, including at the removed singularity.

analytic number theoryprime numbersasymptotics

Source project: Prime Number Theorem and More

Person-level attribution pending.

View proof record