c_mul_im_sq_le_normSq_denom — Mathlib

English

Let c = g_{1,0} and d = g_{1,1}. Then (c Im(z))^2 ≤ || denom(g,z) ||^2.

Русский

Пусть c = g_{1,0}, d = g_{1,1}. Тогда (c·Im(z))^2 ≤ ||denom(g,z)||^2.

LaTeX

$$$((g_{10} \\cdot z.im)^2) \\leq \\operatorname{normSq}(denom(g,z))$$$

Lean4

theorem c_mul_im_sq_le_normSq_denom : (g 1 0 * z.im) ^ 2 ≤ Complex.normSq (denom g z) :=
  by
  set c := g 1 0
  set d := g 1 1
  calc
    (c * z.im) ^ 2 ≤ (c * z.im) ^ 2 + (c * z.re + d) ^ 2 := by nlinarith
    _ = Complex.normSq (denom g z) := by dsimp [c, d, denom, Complex.normSq]; ring

Похожие утверждения