Derivatives of the fundamental-domain boundary contour

Each segment of fdBoundary differentiates in closed form — the verticals and the horizontal to their constant chords, the arcs to the arc speed times the rotated tangent — and away from the segment-junction parameters the contour itself differentiates like its active segment. These are the γ' factors of the valence-formula contour integrals.

Main declarations

• TauCeti.ModularForm.hasDerivAt_fdBoundarySegment1 through TauCeti.ModularForm.hasDerivAt_fdBoundarySegment5: the closed-form segment derivatives.
• TauCeti.ModularForm.hasDerivAt_fdBoundary_of_lt_one … _of_gt_four: the contour differentiates like its active segment between the breakpoints, with the two arcs unified across their smooth junction (hasDerivAt_fdBoundary_of_mem_Ioo_one_three).
• TauCeti.ModularForm.deriv_fdBoundary_four_sub_vertical, …_four_sub_arc: the derivative transforms of the reflection identities of fdBoundary — the γ' halves of the vertical cancellation and the arc self-pairing.

References

• AINTLIB LeanModularForms — the valence-formula development this file ports onto the current Mathlib pin.

theorem TauCeti.ModularForm.hasDerivAt_fdBoundarySegment1 (H t : ℝ) : HasDerivAt (fdBoundarySegment1 H) (↑UpperHalfPlane.ρ + 1 - (1 / 2 + ↑H * Complex.I)) t

Segment 1 differentiates to its constant chord.

theorem TauCeti.ModularForm.hasDerivAt_fdBoundarySegment2 (t : ℝ) : HasDerivAt fdBoundarySegment2 ((Real.pi / 2 - Real.pi / 3) • (circleMap 0 1 (Real.pi / 3 + (t - 1) * (Real.pi / 2 - Real.pi / 3)) * Complex.I)) t

Segment 2 differentiates to the arc speed times the rotated tangent.

theorem TauCeti.ModularForm.hasDerivAt_fdBoundarySegment3 (t : ℝ) : HasDerivAt fdBoundarySegment3 ((2 * Real.pi / 3 - Real.pi / 2) • (circleMap 0 1 (Real.pi / 2 + (t - 2) * (2 * Real.pi / 3 - Real.pi / 2)) * Complex.I)) t

Segment 3 differentiates to the arc speed times the rotated tangent.

theorem TauCeti.ModularForm.hasDerivAt_fdBoundarySegment4 (H t : ℝ) : HasDerivAt (fdBoundarySegment4 H) (-1 / 2 + ↑H * Complex.I - ↑UpperHalfPlane.ρ) t

Segment 4 differentiates to its constant chord.

theorem TauCeti.ModularForm.hasDerivAt_fdBoundarySegment5 (H t : ℝ) : HasDerivAt (fdBoundarySegment5 H) 1 t

Segment 5 differentiates to its constant chord, the unit horizontal.

@[simp]

theorem TauCeti.ModularForm.deriv_fdBoundarySegment1 (H t : ℝ) : deriv (fdBoundarySegment1 H) t = ↑UpperHalfPlane.ρ + 1 - (1 / 2 + ↑H * Complex.I)

Segment 1's derivative, in rewrite form.

@[simp]

theorem TauCeti.ModularForm.deriv_fdBoundarySegment2 (t : ℝ) : deriv fdBoundarySegment2 t = (Real.pi / 2 - Real.pi / 3) • (circleMap 0 1 (Real.pi / 3 + (t - 1) * (Real.pi / 2 - Real.pi / 3)) * Complex.I)

Segment 2's derivative, in rewrite form.

@[simp]

theorem TauCeti.ModularForm.deriv_fdBoundarySegment3 (t : ℝ) : deriv fdBoundarySegment3 t = (2 * Real.pi / 3 - Real.pi / 2) • (circleMap 0 1 (Real.pi / 2 + (t - 2) * (2 * Real.pi / 3 - Real.pi / 2)) * Complex.I)

Segment 3's derivative, in rewrite form.

@[simp]

theorem TauCeti.ModularForm.deriv_fdBoundarySegment4 (H t : ℝ) : deriv (fdBoundarySegment4 H) t = -1 / 2 + ↑H * Complex.I - ↑UpperHalfPlane.ρ

Segment 4's derivative, in rewrite form.

@[simp]

theorem TauCeti.ModularForm.deriv_fdBoundarySegment5 (H t : ℝ) : deriv (fdBoundarySegment5 H) t = 1

Segment 5's derivative, in rewrite form.

theorem TauCeti.ModularForm.hasDerivAt_fdBoundary_of_lt_one {H t : ℝ} (ht : t < 1) : HasDerivAt (fdBoundary H) (↑UpperHalfPlane.ρ + 1 - (1 / 2 + ↑H * Complex.I)) t

Below the first breakpoint the contour differentiates like segment 1.

theorem TauCeti.ModularForm.hasDerivWithinAt_fdBoundary_arc {H t c d : ℝ} (hc : 1 ≤ c) (hd : d ≤ 3) (ht : t ∈ Set.Icc c d) : HasDerivWithinAt (fdBoundary H) ((Real.pi / 6) • (circleMap 0 1 ((t + 1) * (Real.pi / 6)) * Complex.I)) (Set.Icc c d) t

On any subinterval of the arc range, the contour's within-derivative is the arc speed, endpoints included.

theorem TauCeti.ModularForm.hasDerivAt_fdBoundary_of_mem_Ioo_one_three {H t : ℝ} (ht : t ∈ Set.Ioo 1 3) : HasDerivAt (fdBoundary H) ((Real.pi / 6) • (circleMap 0 1 ((t + 1) * (Real.pi / 6)) * Complex.I)) t

Strictly between the first and third breakpoints — across the smooth junction at t = 2, where the two arc segments continue the same circle parameterization — the contour differentiates like the unified arc of angle (t + 1)·π/6.

theorem TauCeti.ModularForm.hasDerivAt_fdBoundary_of_mem_Ioo_three_four {H t : ℝ} (ht : t ∈ Set.Ioo 3 4) : HasDerivAt (fdBoundary H) (-1 / 2 + ↑H * Complex.I - ↑UpperHalfPlane.ρ) t

Strictly between the third and fourth breakpoints the contour differentiates like segment 4.

theorem TauCeti.ModularForm.hasDerivAt_fdBoundary_of_gt_four {H t : ℝ} (ht : 4 < t) : HasDerivAt (fdBoundary H) 1 t

Above the fourth breakpoint the contour differentiates like segment 5.

@[simp]

theorem TauCeti.ModularForm.deriv_fdBoundary_of_lt_one {t H : ℝ} (ht : t < 1) : deriv (fdBoundary H) t = ↑UpperHalfPlane.ρ + 1 - (1 / 2 + ↑H * Complex.I)

The derivative below the first breakpoint, in rewrite form.

@[simp]

theorem TauCeti.ModularForm.deriv_fdBoundary_of_mem_Ioo_one_three {t H : ℝ} (ht : t ∈ Set.Ioo 1 3) : deriv (fdBoundary H) t = (Real.pi / 6) • (circleMap 0 1 ((t + 1) * (Real.pi / 6)) * Complex.I)

The derivative on the unified arc, in rewrite form.

@[simp]

theorem TauCeti.ModularForm.deriv_fdBoundary_of_mem_Ioo_three_four {t H : ℝ} (ht : t ∈ Set.Ioo 3 4) : deriv (fdBoundary H) t = -1 / 2 + ↑H * Complex.I - ↑UpperHalfPlane.ρ

The derivative on the left vertical, in rewrite form.

@[simp]

theorem TauCeti.ModularForm.deriv_fdBoundary_of_gt_four {t H : ℝ} (ht : 4 < t) : deriv (fdBoundary H) t = 1

The derivative above the fourth breakpoint, in rewrite form.

@[simp]

theorem TauCeti.ModularForm.deriv_fdBoundary_four_sub_vertical (H : ℝ) {t : ℝ} (ht : t ∈ Set.Ioo 0 1) : deriv (fdBoundary H) (4 - t) = -deriv (fdBoundary H) t

Differentiating the vertical reflection identity: on the interiors of the verticals, the reflection t ↦ 4 - t negates the derivative.

@[simp]

theorem TauCeti.ModularForm.deriv_fdBoundary_four_sub_arc (H : ℝ) {t : ℝ} (ht : t ∈ Set.Ioo 1 3) : deriv (fdBoundary H) (4 - t) = -deriv (fdBoundary H) t / fdBoundary H t ^ 2

Differentiating the arc reflection identity: on the interior of the arc, the reflection t ↦ 4 - t transforms the derivative by w ↦ -w / z ^ 2 — the inversion z ↦ -1/z contributes its derivative w ↦ w / z ^ 2, and the parameter reversal t ↦ 4 - t contributes the minus sign.

@[simp]

theorem TauCeti.ModularForm.logDeriv_fdBoundary_arc {H t : ℝ} (ht : t ∈ Set.Ioo 1 3) : logDeriv (fdBoundary H) t = ↑(Real.pi / 6) * Complex.I

On the open arc the contour's logarithmic derivative — its logarithmic speed γ' / γ — is the constant π/6 · i: the arc traverses the unit circle at angular speed π/6.

theorem TauCeti.ModularForm.integral_logDeriv_fdBoundary_arc (H : ℝ) {a b : ℝ} (ha : a ∈ Set.Icc 1 3) (hb : b ∈ Set.Icc 1 3) : ∫ (t : ℝ) in a..b, logDeriv (fdBoundary H) t = (↑b - ↑a) * (↑(Real.pi / 6) * Complex.I)

The arc integral of the contour's logarithmic derivative over any subinterval of the arc, in either orientation: the integrand is π/6 · i on the open arc (logDeriv_fdBoundary_arc), hence almost everywhere for these interval integrals.

theorem TauCeti.ModularForm.intervalIntegrable_logDeriv_fdBoundary_arc (H : ℝ) {a b : ℝ} (ha : a ∈ Set.Icc 1 3) (hb : b ∈ Set.Icc 1 3) : IntervalIntegrable (logDeriv (fdBoundary H)) MeasureTheory.volume a b

The contour's logarithmic derivative is interval-integrable on arc subintervals: it is the constant π/6 · i on the open arc.

theorem TauCeti.ModularForm.intervalIntegral_comp_fdBoundary_four_sub {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (H : ℝ) (φ : ℂ → E) {a b : ℝ} : ∫ (t : ℝ) in 4 - b..4 - a, deriv (fdBoundary H) t • φ (fdBoundary H t) = ∫ (u : ℝ) in a..b, deriv (fdBoundary H) (4 - u) • φ (fdBoundary H (4 - u))

Substituting the reflection t ↦ 4 - t in a boundary contour integral.