Distance of the boundary contour from ρ

The geometry of the shifted contour t ↦ fdBoundary H t - ρ about the corner ρ at parameter t = 3: the chord distance along the arc, the purely imaginary linear form along the left vertical, the norm lower bounds on the far pieces, the slit-plane confinement of every piece, and the exact polar forms and principal logarithms of the shifted contour beside the corner. The corner joins the arc to the vertical at the interior angle π/3, which is exactly the gap between the two one-sided argument limits π/6 and π/2 — the source of the winding value -1/6 at ρ.

Main declarations

• TauCeti.ModularForm.norm_fdBoundary_sub_rho_arc (the chord distance).
• TauCeti.ModularForm.fdBoundary_sub_rho_of_mem_Icc_three_four (the linear form).
• TauCeti.ModularForm.log_fdBoundary_three_sub_sub_rho, TauCeti.ModularForm.log_fdBoundary_three_add_sub_rho (the endpoint logarithms).

References

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

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

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

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

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

theorem TauCeti.ModularForm.norm_fdBoundary_sub_rho_segment1 {t : ℝ} (H : ℝ) (ht : t ∈ Set.Icc 0 1) : 1 ≤ ‖fdBoundary H t - ↑UpperHalfPlane.ρ‖

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

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

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

theorem TauCeti.ModularForm.fdBoundary_sub_rho_mem_slitPlane_of_le_one {t : ℝ} (H : ℝ) (ht : t ∈ Set.Icc 0 1) : fdBoundary H t - ↑UpperHalfPlane.ρ ∈ Complex.slitPlane

Right of the corner column the shifted contour has real part 1: slit plane.

theorem TauCeti.ModularForm.fdBoundary_sub_rho_arc_mem_slitPlane_of_lt_three {t : ℝ} (H : ℝ) (ht1 : 1 ≤ t) (ht3 : t < 3) : fdBoundary H t - ↑UpperHalfPlane.ρ ∈ Complex.slitPlane

Before the corner the arc stays right of the corner column: the real part of the shifted contour is cos((t+1)·π/6) + 1/2 > 0, so it lies in the slit plane.

theorem TauCeti.ModularForm.fdBoundary_sub_rho_mem_slitPlane_of_three_lt {H t : ℝ} (hH : √3 / 2 < H) (ht3 : 3 < t) (ht4 : t ≤ 4) : fdBoundary H t - ↑UpperHalfPlane.ρ ∈ Complex.slitPlane

Above the corner the left vertical is purely imaginary of positive height: slit plane.

theorem TauCeti.ModularForm.fdBoundary_sub_rho_mem_slitPlane_of_mem_Icc_four_five {H t : ℝ} (hH : √3 / 2 < H) (ht : t ∈ Set.Icc 4 5) : fdBoundary H t - ↑UpperHalfPlane.ρ ∈ Complex.slitPlane

On the ceiling the shifted contour has height H - √3/2 > 0: slit plane.

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

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

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

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

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

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