[KADIRI]: Expressing the contour integral as a rectangular integral (equation (12))

[teorth]

Description

Should follow from Laplace inversion and rearranging sums. Main difficulty is to justify interchange of the summation and contour integral.

Blueprint

Sublemma 8.5.3

Zulip

Link

[giuseppesorge]

Possible missing hypothesis on T in kadiri_thm_3_1_q1_eq_12

I've been formalizing eq. (12) (the rectangle decomposition of I(T)) and I think the statement may need an extra hypothesis on T.

The proof applies the residue theorem to (-ζ'/ζ)(s)·Φ(-s) on the rectangle with corners ±a ± iT. This requires the integrand to have no poles on the rectangle border — in particular, no nontrivial zero ρ of ζ with Im ρ = ±T exactly. The current hypotheses only assume 0 < T, which doesn't rule this out.

Concretely, if some zero ρ₀ has Im ρ₀ = T, then (a) the top horizontal integral ∫_{-a+iT}^{1+a+iT} passes through the pole at ρ₀, and (b) ρ₀ is excluded from the residue sum zeroes_sum (.Ioo 0 1) (.Ioo (-T) T) since the imaginary interval is open at T. So the identity as stated seems ill-posed at such T.

Would you prefer to add a hypothesis like ∀ ρ, ζ ρ = 0 → ρ.im ≠ T ∧ ρ.im ≠ -T (i.e. T is not the ordinate of a zero), or handle it another way? I have the rest of the proof essentially ready (Laplace-transform analyticity of Φ, the rectangle/residue reduction, etc.) and just want to match the intended statement before finalizing.

[Robby955]

T needs to avoid the zero ordinates for the rectangle argument.

A clean statement is to add a hypothesis that no nontrivial zero ρ has Im ρ = T (i.e. T is not in {Im ρ : ρ a
zero in the strip}); that keeps the top and bottom borders pole-free and the residue sum well-defined.
On the downstream effect: the capstone only uses eq-12 through the I(T) → ∞ limit and the two horizontal-vanishing lemmas, all stated along atTop, and the off-ordinate heights are cofinal, so restricting to such T does not weaken Théorème 3.1.

[giuseppesorge]

Thanks @Robby955 — that matches what I found, I'll add the hypothesis that no nontrivial zero ρ has ρ.im = T (in the ρ.im ≠ T ∧ ρ.im ≠ -T / off-ordinate form).

One architectural question before I open the PR. My proof reduces eq. (12) to the rectangle residue theorem RectangleIntegral'_eq_sumResiduesIn (together with residue / sumResiduesIn), which currently live in IEANTN/CH2/CH2.lean. To use them from Kadiri.lean I can either:

(a) import the whole CH2 module into Kadiri.lean, or
(b) extract those general rectangle-residue lemmas into a shared file (e.g. ResidueCalcOnRectangles.lean) and have both CH2 and Kadiri import them.

(b) seems architecturally cleaner, but it touches CH2.lean (which has the open PR #1572). Do you have a preference, or would you rather these residue lemmas stay where they are for now?

(For context, the rest of eq. (12) is essentially ready on my side: meromorphy of ζ, analyticity of the Laplace transform Φ on the strip, -ζ'/ζ having only simple poles with residue equal to the order, and the rectangle decomposition — all sorry-free.)

[Robby955]

Since those are general residue lemmas, so they might belong in ResidueCalcOnRectangles.lean next to RectangleIntegral' rather than behind a full CH2 import. Given #1572, a small standalone extraction PR first could be a clean way to do it, but I am only a contributor, maintainers may have other plans or directions.

[giuseppesorge]

@teorth — quick architecture question (you set up the IEANTN folder in #1463 and coordinate these). My eq. (12) proof reduces to the rectangle residue theorem RectangleIntegral'_eq_sumResiduesIn (+ residue / sumResiduesIn / HasSimplePolesOn), currently in IEANTN/CH2/CH2.lean. As @Robby955 noted, these look general enough to live in ResidueCalcOnRectangles.lean next to RectangleIntegral', letting Kadiri.lean use them without a full CH2 import.

Would you prefer (a) a small standalone PR extracting those general residue lemmas into ResidueCalcOnRectangles.lean (CH2 then imports them), or (b) keep them in CH2 for now and have Kadiri import CH2? Happy to do whichever fits your plans for the folder. (#1572 also touches CH2.lean, so I'd sequence to avoid conflicts.)

[teorth]

I would favor moving any generally reusable contour integration lemmas into ResidueCalcOnRectangles.lean.

[giuseppesorge]

propose #1608