English
For a given coprime bottom row cd there exists g ∈ SL(2,ℤ) with g1 = cd that minimizes |(g•z).re| among all matrices with bottom row equal to cd.
Русский
Для данного coprime нижнего ряда cd существует g ∈ SL(2,ℤ) с g1 = cd, минимизирующий |Re(g•z)| по всем матрицам с данным нижним рядом.
LaTeX
$$$\\exists g\\in SL(2,\\mathbb{Z}),\\; g_1 = cd \\land \\forall g'\\in SL(2,\\mathbb{Z}),\\; g_1 = g'_1 \\Rightarrow |\\Re(g\\cdot z)| \\le |\\Re(g'\\cdot z)|.$$$
Lean4
/-- Given `z : ℍ` and a bottom row `(c,d)`, among the `g : SL(2,ℤ)` with this bottom row, minimize
`|(g•z).re|`. -/
theorem exists_row_one_eq_and_min_re {cd : Fin 2 → ℤ} (hcd : IsCoprime (cd 0) (cd 1)) :
∃ g : SL(2, ℤ), g 1 = cd ∧ ∀ g' : SL(2, ℤ), g 1 = g' 1 → |(g • z).re| ≤ |(g' • z).re| :=
by
haveI : Nonempty { g : SL(2, ℤ) // g 1 = cd } :=
let ⟨x, hx⟩ := bottom_row_surj hcd
⟨⟨x, hx.2⟩⟩
obtain ⟨g, hg⟩ := Filter.Tendsto.exists_forall_le (tendsto_abs_re_smul z hcd)
refine ⟨g, g.2, ?_⟩
intro g1 hg1
have : g1 ∈ (fun g : SL(2, ℤ) => g 1) ⁻¹' { cd } :=
by
rw [Set.mem_preimage, Set.mem_singleton_iff]
exact Eq.trans hg1.symm (Set.mem_singleton_iff.mp (Set.mem_preimage.mp g.2))
exact hg ⟨g1, this⟩
