The excised boundary contour integral of a level-one logarithmic derivative

TauCeti.ModularForm.intervalIntegral_logDeriv_fdBoundary assembles the boundary integral for a form with no zeros on the contour. The valence formula needs the version that tolerates them at the elliptic points i and ρ, which sit on the fundamental-domain boundary, so a form vanishing there makes logDeriv f blow up on the contour itself. (Nonvanishing along the ceiling is still required, through the q-disk hypothesis.) The device is ε-excision — the integrand is replaced by 0 within ε of any excision centre — and this file assembles the excised integral at a fixed ε, from integrability hypotheses it takes rather than proves. Taking ε → 0 and identifying the limit as a principal value is not done here.

The three pieces are already available and each already tolerates the excision: the verticals cancel by periodicity (intervalIntegral_excised_fdBoundarySegment4_eq_neg_segment1), the arc collapses to its weight term (two_mul_intervalIntegral_excised_deriv_smul_logDeriv_comp_ofComplex_fdBoundary_arc), and the ceiling is untouched by the excision altogether (intervalIntegral_excised_logDeriv_fdBoundarySegment5_eq_two_pi_I_mul_qExpansionOrderAtCusp).

The assembly comes in two set shapes. intervalIntegral_excised_logDeriv_fdBoundary takes a single unit-norm inversion-closed excision set, which serves a form whose contour zeros all sit on the arc. The valence formula's unconditional excision set is the union arcSingularSet S ∪ verticalSingularSet S, whose vertical part leaves the unit circle; intervalIntegral_excised_logDeriv_fdBoundary_arcSingularSet_union_verticalSingularSet assembles that shape. Its verticals still cancel — the union is closed under the reflection z ↦ -conj z — and once ε is under the arc/vertical separation the union test agrees with its arc part along the arc, so the arc still collapses through the arc-only machinery.

Main declarations

• TauCeti.ModularForm.intervalIntegral_excised_logDeriv_fdBoundary: the assembled excised boundary integral, 2πi · ord_∞ - (k/2) · ∫₁³ (excised logDeriv γ).
• intervalIntegral_excised_logDeriv_fdBoundary_arcSingularSet_union_verticalSingularSet (same namespace): the assembly for the union-shaped excision set, for ε under the arc/vertical separation.

References

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

theorem TauCeti.ModularForm.intervalIntegral_excised_logDeriv_fdBoundary {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {k : ℤ} [SlashInvariantFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k] (f : F) (hS : ModularGroup.S ∈ Γ) {H ε : ℝ} {S : Finset ℂ} (hnorm : ∀ s ∈ S, ‖s‖ = 1) (hinv : ∀ s ∈ S, -1 / s ∈ S) (hlt : ∀ s ∈ S, s.im + ε < H) (hper : Function.Periodic (⇑f ∘ ↑UpperHalfPlane.ofComplex) 1) (hd : ∀ t ∈ Set.Ioo 1 2, (¬∃ s ∈ S, ‖fdBoundary H t - s‖ ≤ ε) → DifferentiableAt ℂ (⇑f ∘ ↑UpperHalfPlane.ofComplex) (fdBoundary H t)) (hne : ∀ t ∈ Set.Ioo 1 2, (¬∃ s ∈ S, ‖fdBoundary H t - s‖ ≤ ε) → (⇑f ∘ ↑UpperHalfPlane.ofComplex) (fdBoundary H t) ≠ 0) (hga : ∀ q ∈ Metric.closedBall 0 (fdBoundaryQRadius H), AnalyticAt ℂ (UpperHalfPlane.cuspFunction 1 ⇑f) q) (hgz : ∀ q ∈ Metric.closedBall 0 (fdBoundaryQRadius H), q ≠ 0 → UpperHalfPlane.cuspFunction 1 (⇑f) q ≠ 0) (hint01 : IntervalIntegrable (fun (t : ℝ) => if ∃ s ∈ S, ‖fdBoundary H t - s‖ ≤ ε then 0 else deriv (fdBoundary H) t • logDeriv (⇑f ∘ ↑UpperHalfPlane.ofComplex) (fdBoundary H t)) MeasureTheory.volume 0 1) (hint12 : IntervalIntegrable (fun (t : ℝ) => if ∃ s ∈ S, ‖fdBoundary H t - s‖ ≤ ε then 0 else deriv (fdBoundary H) t • logDeriv (⇑f ∘ ↑UpperHalfPlane.ofComplex) (fdBoundary H t)) MeasureTheory.volume 1 2) (hint45 : IntervalIntegrable (fun (t : ℝ) => if ∃ s ∈ S, ‖fdBoundary H t - s‖ ≤ ε then 0 else deriv (fdBoundary H) t • logDeriv (⇑f ∘ ↑UpperHalfPlane.ofComplex) (fdBoundary H t)) MeasureTheory.volume 4 5) : (∫ (t : ℝ) in 0..5, if ∃ s ∈ S, ‖fdBoundary H t - s‖ ≤ ε then 0 else deriv (fdBoundary H) t • logDeriv (⇑f ∘ ↑UpperHalfPlane.ofComplex) (fdBoundary H t)) = 2 * ↑Real.pi * Complex.I * ↑(qExpansionOrderAtCusp 1 ⇑f) - ↑k / 2 * ∫ (t : ℝ) in 1..3, if ∃ s ∈ S, ‖fdBoundary H t - s‖ ≤ ε then 0 else logDeriv (fdBoundary H) t

The excised boundary contour integral of a level-one logarithmic derivative. The four pieces assemble exactly as they do without the excision: the verticals cancel, the arc collapses to its weight term, and the ceiling reads the cusp order. What the excision buys is zeros on the arc and at the elliptic boundary points, where the integrand is replaced by 0 instead. It does not free the ceiling: hgz still asks f to be nonvanishing at every nonzero point of the closed q-disk, the circle of which is the ceiling.

The statement is at a fixed ε, with integrability on [0, 1], [1, 2] and [4, 5] assumed; the remaining two pieces are derived by the reflections. Compare intervalIntegral_logDeriv_fdBoundary, the unexcised assembly, whose arc term is the constant k·(π/6)·i: here the arc term is (k/2) times the excised arc integral of the contour's own logarithmic derivative, an ε-dependent quantity this theorem says nothing about the limit of.

theorem TauCeti.ModularForm.intervalIntegral_excised_logDeriv_fdBoundary_arcSingularSet_union_verticalSingularSet {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {k : ℤ} [SlashInvariantFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k] (f : F) (hS : ModularGroup.S ∈ Γ) {H ε : ℝ} {S : Finset UpperHalfPlane} (hfar : ∀ s ∈ verticalSingularSet S, s ∉ arcSingularSet S → ∀ t ∈ Set.Icc 1 3, ε < ‖fdBoundary H t - s‖) (hlt : ∀ s ∈ arcSingularSet S ∪ verticalSingularSet S, s.im + ε < H) (hper : Function.Periodic (⇑f ∘ ↑UpperHalfPlane.ofComplex) 1) (hd : ∀ t ∈ Set.Ioo 1 2, (¬∃ s ∈ arcSingularSet S ∪ verticalSingularSet S, ‖fdBoundary H t - s‖ ≤ ε) → DifferentiableAt ℂ (⇑f ∘ ↑UpperHalfPlane.ofComplex) (fdBoundary H t)) (hne : ∀ t ∈ Set.Ioo 1 2, (¬∃ s ∈ arcSingularSet S ∪ verticalSingularSet S, ‖fdBoundary H t - s‖ ≤ ε) → (⇑f ∘ ↑UpperHalfPlane.ofComplex) (fdBoundary H t) ≠ 0) (hga : ∀ q ∈ Metric.closedBall 0 (fdBoundaryQRadius H), AnalyticAt ℂ (UpperHalfPlane.cuspFunction 1 ⇑f) q) (hgz : ∀ q ∈ Metric.closedBall 0 (fdBoundaryQRadius H), q ≠ 0 → UpperHalfPlane.cuspFunction 1 (⇑f) q ≠ 0) (hint01 : IntervalIntegrable (fun (t : ℝ) => if ∃ s ∈ arcSingularSet S ∪ verticalSingularSet S, ‖fdBoundary H t - s‖ ≤ ε then 0 else deriv (fdBoundary H) t • logDeriv (⇑f ∘ ↑UpperHalfPlane.ofComplex) (fdBoundary H t)) MeasureTheory.volume 0 1) (hint12 : IntervalIntegrable (fun (t : ℝ) => if ∃ s ∈ arcSingularSet S ∪ verticalSingularSet S, ‖fdBoundary H t - s‖ ≤ ε then 0 else deriv (fdBoundary H) t • logDeriv (⇑f ∘ ↑UpperHalfPlane.ofComplex) (fdBoundary H t)) MeasureTheory.volume 1 2) (hint45 : IntervalIntegrable (fun (t : ℝ) => if ∃ s ∈ arcSingularSet S ∪ verticalSingularSet S, ‖fdBoundary H t - s‖ ≤ ε then 0 else deriv (fdBoundary H) t • logDeriv (⇑f ∘ ↑UpperHalfPlane.ofComplex) (fdBoundary H t)) MeasureTheory.volume 4 5) : (∫ (t : ℝ) in 0..5, if ∃ s ∈ arcSingularSet S ∪ verticalSingularSet S, ‖fdBoundary H t - s‖ ≤ ε then 0 else deriv (fdBoundary H) t • logDeriv (⇑f ∘ ↑UpperHalfPlane.ofComplex) (fdBoundary H t)) = 2 * ↑Real.pi * Complex.I * ↑(qExpansionOrderAtCusp 1 ⇑f) - ↑k / 2 * ∫ (t : ℝ) in 1..3, if ∃ s ∈ arcSingularSet S ∪ verticalSingularSet S, ‖fdBoundary H t - s‖ ≤ ε then 0 else logDeriv (fdBoundary H) t

The excised boundary integral for the union-shaped excision set. The excision set is now arcSingularSet S ∪ verticalSingularSet S — both singular families of a finite set of upper half-plane points — rather than a single unit-norm inversion-closed set, so a form may vanish on the verticals of the contour as well as on the arc. The verticals still cancel: the union is closed under the reflection z ↦ -conj z that exchanges them (neg_conj_mem_arcSingularSet_union_verticalSingularSet). The arc still collapses to its weight term: for ε under the arc/vertical separation hfar the union test agrees with its arc part along the arc, and the arc-only pairing machinery applies. The ceiling is untouched by the excision, exactly as in intervalIntegral_excised_logDeriv_fdBoundary.

hfar is the fixed-ε reading of the separation exists_pos_forall_le_norm_fdBoundary_sub_of_mem_verticalSingularSet, satisfied for every small ε by eventually_forall_lt_norm_fdBoundary_sub_of_mem_verticalSingularSet; hlt is the same ε-smallness clearance below the ceiling the arc-only assembly takes.