English
For any real c and d with 1 ≤ d^2, we have r1(z) ≤ (c Re z + d)^2 + (c Im z)^2.
Русский
Для любых c, d ∈ ℝ с 1 ≤ d^2 выполняется r1(z) ≤ (c Re z + d)^2 + (c Im z)^2.
LaTeX
$$$\\forall z \\in \\mathbb{H},\\; \\forall c,d \\in \\mathbb{R},\\; 1 \\le d^2 \\Rightarrow r_1(z) \\le (c \\operatorname{Re} z + d)^2 + (c \\operatorname{Im} z)^2$$$
Lean4
/-- For `c, d ∈ ℝ` with `1 ≤ d ^ 2`, we have `r1 z ≤ |c * z + d| ^ 2`. -/
theorem r1_aux_bound (c : ℝ) {d : ℝ} (hd : 1 ≤ d ^ 2) : r1 z ≤ (c * z.re + d) ^ 2 + (c * z.im) ^ 2 :=
by
have H1 : (c * z.re + d) ^ 2 + (c * z.im) ^ 2 = c ^ 2 * (z.re ^ 2 + z.im ^ 2) + d * 2 * c * z.re + d ^ 2 := by ring
have H2 :
(c ^ 2 * (z.re ^ 2 + z.im ^ 2) + d * 2 * c * z.re + d ^ 2) * (z.re ^ 2 + z.im ^ 2) - z.im ^ 2 =
(c * (z.re ^ 2 + z.im ^ 2) + d * z.re) ^ 2 + (d ^ 2 - 1) * z.im ^ 2 :=
by ring
rw [r1, H1, div_le_iff₀ (by positivity), ← sub_nonneg, H2]
exact add_nonneg (sq_nonneg _) (mul_nonneg (sub_nonneg.mpr hd) (sq_nonneg _))
