The vertical integrals of a periodic integrand cancel

The reflection t ↦ 4 - t carries the right vertical of the boundary contour onto the left vertical through the translation z ↦ z - 1, reversing the orientation. For any integrand φ of period 1 — the level-one situation, where φ is the logarithmic derivative of the extension of a modular form — the left vertical contour integral of γ' • φ ∘ γ is therefore the negative of the right one: the values are identified by periodicity and the derivatives by the reflection, up to the orientation sign. The statement is unconditional: the substitution and the interior congruence need no integrability.

The cancellation also survives ε-excision, which is what the principal-value assembly of the valence formula needs: when the form vanishes at a point on the contour the integrand is not interval-integrable there, so the boundary integral is assembled from an excised integrand and the limit taken only after the pieces are combined. The excised cancellation holds whenever the excision set is invariant under the reflection z ↦ -conj z that exchanges the two verticals — reflection invariance, not translation closure, is the usable hypothesis, since a finite set closed under s ↦ s + 1 is empty.

Main declarations

• TauCeti.ModularForm.intervalIntegral_fdBoundarySegment4_eq_neg_segment1.
• TauCeti.ModularForm.intervalIntegral_excised_fdBoundarySegment4_eq_neg_segment1: the same cancellation for a reflection-invariantly excised integrand.

References

• AINTLIB LeanModularForms — the valence-formula development (ForMathlib/ValenceFormula/PVChain/Assembly.lean, the vertical cancellation) this file ports onto the current Mathlib pin.

theorem TauCeti.ModularForm.intervalIntegral_fdBoundarySegment4_eq_neg_segment1 {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (H : ℝ) {φ : ℂ → E} (hφ : Function.Periodic φ 1) : ∫ (t : ℝ) in 3..4, deriv (fdBoundary H) t • φ (fdBoundary H t) = -∫ (t : ℝ) in 0..1, deriv (fdBoundary H) t • φ (fdBoundary H t)

The left vertical integral of a period-1 integrand along the boundary contour is the negative of the right vertical integral: the reflection t ↦ 4 - t carries the right vertical onto the left through the translation z ↦ z - 1, which the periodicity absorbs, and reverses the orientation.

theorem TauCeti.ModularForm.intervalIntegrable_deriv_smul_fdBoundarySegment4 {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {H : ℝ} {φ : ℂ → E} (hφ : Function.Periodic φ 1) (hint : IntervalIntegrable (fun (t : ℝ) => deriv (fdBoundary H) t • φ (fdBoundary H t)) MeasureTheory.volume 0 1) : IntervalIntegrable (fun (t : ℝ) => deriv (fdBoundary H) t • φ (fdBoundary H t)) MeasureTheory.volume 3 4

The right-vertical integrability of a period-1 integrand reflects to the left vertical: the reflection carries the integrand to its negation through the translation and the periodicity.

theorem TauCeti.ModularForm.exists_norm_fdBoundary_four_sub_le_iff {H : ℝ} {S : Finset ℂ} {ε : ℝ} (hrefl : ∀ s ∈ S, -(starRingEnd ℂ) s ∈ S) {u : ℝ} (hu : u ∈ Set.Ioo 0 1) : (∃ s ∈ S, ‖fdBoundary H (4 - u) - s‖ ≤ ε) ↔ ∃ s ∈ S, ‖fdBoundary H u - s‖ ≤ ε

The excision test is invariant under the vertical reflection. On the verticals the substitution t ↦ 4 - t acts as z ↦ -conj z, since there the real part is ±1/2. That map is an isometry of ℂ, so it carries the ε-ball around a centre to the ε-ball around the reflected centre; for an excision set closed under the reflection the test therefore reads the same at 4 - u as at u.

Reflection invariance, not translation closure, is the right hypothesis: a finite set closed under s ↦ s + 1 would have to be empty, since it has an element of largest real part.

theorem TauCeti.ModularForm.intervalIntegrable_excised_deriv_smul_fdBoundarySegment4 {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {H : ℝ} {φ : ℂ → E} (hφ : Function.Periodic φ 1) {S : Finset ℂ} {ε : ℝ} (hrefl : ∀ s ∈ S, -(starRingEnd ℂ) s ∈ S) (hint : IntervalIntegrable (fun (t : ℝ) => deriv (fdBoundary H) t • if ∃ s ∈ S, ‖fdBoundary H t - s‖ ≤ ε then 0 else φ (fdBoundary H t)) MeasureTheory.volume 0 1) : IntervalIntegrable (fun (t : ℝ) => deriv (fdBoundary H) t • if ∃ s ∈ S, ‖fdBoundary H t - s‖ ≤ ε then 0 else φ (fdBoundary H t)) MeasureTheory.volume 3 4

Integrability on the left vertical, excised. The reflection t ↦ 4 - t carries the right vertical onto the left, and it carries the excised integrand to itself: the excision test transports by exists_norm_fdBoundary_four_sub_le_iff, and the integrand's value by the periodicity already used without the excision.

theorem TauCeti.ModularForm.intervalIntegral_excised_fdBoundarySegment4_eq_neg_segment1 {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (H : ℝ) {φ : ℂ → E} (hφ : Function.Periodic φ 1) {S : Finset ℂ} {ε : ℝ} (hrefl : ∀ s ∈ S, -(starRingEnd ℂ) s ∈ S) : (∫ (t : ℝ) in 3..4, deriv (fdBoundary H) t • if ∃ s ∈ S, ‖fdBoundary H t - s‖ ≤ ε then 0 else φ (fdBoundary H t)) = -∫ (t : ℝ) in 0..1, deriv (fdBoundary H) t • if ∃ s ∈ S, ‖fdBoundary H t - s‖ ≤ ε then 0 else φ (fdBoundary H t)

The vertical cancellation survives excision. The reflection t ↦ 4 - t carries the right vertical onto the left by z ↦ -conj z, an isometry of ℂ, so an integrand excised within ε of a set invariant under that reflection is excised at matching parameters on the two verticals, and the cancellation of the untruncated integrals (TauCeti.ModularForm.intervalIntegral_fdBoundarySegment4_eq_neg_segment1) persists.

Reflection invariance, not translation closure, is the right hypothesis: the two verticals are exchanged by z ↦ -conj z, and being an isometry it moves an ε-ball to an ε-ball. (A set closed under the bare translation s ↦ s + 1 would have to be empty, since a finite set has an element of largest real part.) For TauCeti.ModularForm.verticalSingularSet the invariance is the composite of re_eq_of_mem_verticalSingularSet with sub_one_mem_verticalSingularSet or add_one_mem_verticalSingularSet, whose translations are conditional on the real part.