Documentation

TauCeti.NumberTheory.ModularForms.LevelOne.FundamentalDomainBoundary.Winding.Rho.AddOne.Geometry

Distance of the boundary contour from ρ + 1 #

The geometry of the shifted contour t ↦ fdBoundary H t - (ρ + 1) about the corner ρ + 1 at parameter t = 1: the purely imaginary linear form along the right vertical, the chord distance along the arc, the norm lower bounds on the far pieces, the closed-upper-half-plane confinement — and the exact endpoint logarithms beside the corner.

The confinement holds only once the ceiling clears the corner row, and the confinement results accordingly carry √3/2 ≤ H. Under that hypothesis the shifted contour touches the branch cut at t = 3, where its value is -1, but never crosses it; at the degenerate height H = √3/2 the whole left vertical degenerates to that point and lies on the cut throughout. Below the corner row the claim fails outright: on the left vertical the shifted contour is -1 + (t - 3)(H - √3/2)i, so for H < √3/2 the imaginary part is negative immediately after t = 3 and the contour does cross the cut.

The corner joins the vertical to the arc at the interior angle π/3, which is exactly the gap between the one-sided argument limits π/2 and 5π/6 — the source of the winding value -1/6 at ρ + 1.

Main declarations #

References #

source
theorem TauCeti.ModularForm.rho_add_one_im :
(↑UpperHalfPlane.ρ + 1).im = √3 / 2

The corner ρ + 1 sits on the same row Im = √3/2 as ρ: the shift is by a real number, which does not move the imaginary part.

Not @[simp], for the same reason as rho_im: simp reaches ρ.im through Complex.add_im, UpperHalfPlane.coe_im and Complex.one_im before this could fire.

source
theorem TauCeti.ModularForm.fdBoundary_sub_rho_add_one_of_mem_Icc_zero_one {t : ℝ} (H : ℝ) (ht : t ∈ Set.Icc 0 1) :
fdBoundary H t - (↑UpperHalfPlane.ρ + 1) = ↑((1 - t) * (H - √3 / 2)) * Complex.I

On the right vertical the shifted contour is the purely imaginary linear form (1 - t)·(H - √3/2)·i.

source
theorem TauCeti.ModularForm.norm_fdBoundary_sub_rho_add_one_arc {t : ℝ} (H : ℝ) (ht : t ∈ Set.Icc 1 3) :
‖fdBoundary H t - (↑UpperHalfPlane.ρ + 1)‖ = 2 * |Real.sin ((t - 1) * (Real.pi / 12))|

On the arc the distance from ρ + 1 is the chord distance: 2·sin(|t - 1|·π/12) up to the absolute value inside the sine.

source
theorem TauCeti.ModularForm.norm_fdBoundary_sub_rho_add_one_arc_le {δ t : ℝ} (H : ℝ) (ht : t ∈ Set.Icc 1 3) (hδ : δ ≤ 6) (hle : t - 1 ≤ δ) :
‖fdBoundary H t - (↑UpperHalfPlane.ρ + 1)‖ ≤ 2 * Real.sin (δ * (Real.pi / 12))

Along the arc the chord to ρ + 1 grows with the parameter. A point of the arc at parameter t is no further from the corner than the point at parameter 1 + δ is, whose chord is 2·sin(δ·π/12).

This is the generic monotonicity of a chord in the angular gap, TauCeti.dist_circleMap_le_dist_circleMap_of_abs_sub_le, read along the arc, whose parameter runs at π/6 per unit; δ ≤ 6 keeps the comparison point within half a turn of the corner, where the chord is still increasing.

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

On the left vertical the shifted contour is -1 plus the imaginary linear form of the ρ-shift, so its real part is constantly -1 and it runs alongside the branch cut. Where the ceiling misses the corner row the imaginary part vanishes only at t = 3, so the cut is met there alone — above it when the ceiling clears the row, below it otherwise. At the degenerate height H = √3/2 the imaginary part vanishes identically and the whole segment is the point -1, lying on the cut throughout.

source
theorem TauCeti.ModularForm.norm_fdBoundary_sub_rho_add_one_segment4 {t : ℝ} (H : ℝ) (ht : t ∈ Set.Icc 3 4) :
1 ≤ ‖fdBoundary H t - (↑UpperHalfPlane.ρ + 1)‖

On the left vertical the contour keeps distance at least 1 from ρ + 1: the real parts differ by exactly 1.

source
theorem TauCeti.ModularForm.norm_fdBoundary_sub_rho_add_one_segment5 {H t : ℝ} (ht : t ∈ Set.Icc 4 5) :
|H - √3 / 2| ≤ ‖fdBoundary H t - (↑UpperHalfPlane.ρ + 1)‖

On the ceiling the contour keeps distance at least |H - √3/2| from ρ + 1. The absolute value is what the height difference gives, and it is the only form with content below the corner row, where H - √3/2 < 0 makes the signed bound vacuous.

source
theorem TauCeti.ModularForm.im_fdBoundary_sub_rho_add_one_arc_nonneg {t : ℝ} (H : ℝ) (ht : t ∈ Set.Icc 1 3) :
0 ≤ (fdBoundary H t - (↑UpperHalfPlane.ρ + 1)).im

On the arc the shifted contour stays in the closed upper half-plane.

source
theorem TauCeti.ModularForm.im_fdBoundary_sub_rho_add_one_arc_pos {t : ℝ} (H : ℝ) (ht1 : 1 < t) (ht3 : t < 3) :
0 < (fdBoundary H t - (↑UpperHalfPlane.ρ + 1)).im

Strictly inside the arc the shifted contour has positive height.

source
theorem TauCeti.ModularForm.im_fdBoundary_sub_rho_add_one_nonneg {H t : ℝ} (hH : √3 / 2 ≤ H) (ht : t ∈ Set.Icc 0 5) :
0 ≤ (fdBoundary H t - (↑UpperHalfPlane.ρ + 1)).im

The shifted contour stays in the closed upper half-plane over the whole parameter range: the contour clears the corner row √3/2, which is the height of ρ + 1.

source
theorem TauCeti.ModularForm.log_fdBoundary_one_sub_sub_rho_add_one {H δ : ℝ} (hH : √3 / 2 < H) (hδ : 0 < δ) (hδ2 : δ ≤ 1) :
Complex.log (fdBoundary H (1 - δ) - (↑UpperHalfPlane.ρ + 1)) = ↑(Real.log (δ * (H - √3 / 2))) + ↑(Real.pi / 2) * Complex.I

The principal logarithm of the shifted contour just before the corner.

source
theorem TauCeti.ModularForm.log_fdBoundary_one_add_sub_rho_add_one {δ : ℝ} (H : ℝ) (hδ : 0 < δ) (hδ2 : δ ≤ 2) :
Complex.log (fdBoundary H (1 + δ) - (↑UpperHalfPlane.ρ + 1)) = ↑(Real.log (2 * Real.sin (δ * (Real.pi / 12)))) + ↑(5 * Real.pi / 6 + δ * (Real.pi / 12)) * Complex.I

The principal logarithm of the shifted contour just after the corner.

source
theorem TauCeti.ModularForm.eq_one_of_fdBoundary_eq_rho_add_one {H t : ℝ} (hH : H ≠ √3 / 2) (ht : t ∈ Set.Icc 0 5) (heq : fdBoundary H t = ↑UpperHalfPlane.ρ + 1) :
t = 1

The contour passes through ρ + 1 only at the corner t = 1.