English
A nonzero polynomial f ∈ ℤ[X] relates irrational roots to Liouville-type bounds; this is a technical lemma used in the Liouville-Weierstrass framework, establishing a link between roots of polynomials and exponential approximations via complex analysis.
Русский
Не нулевой многочлен f над целыми связывает иррациональные корни с ограничениями Лиоуille по экспонентам; техническая лемма в рамках теории Лиувилля–Вейерштрасса.
LaTeX
$$$\\text{exp_polynomial_approx}$, a technical lemma describing the construction of auxiliary bounds linking roots of $f$ to exponential expressions, used in Liouville–Weierstrass argument.$$
Lean4
/-- A (positive) natural number `n` is a sum of two squares if and only if the exponent of
every prime `q` such that `q % 4 = 3` in the prime factorization of `n` is even.
(The assumption `0 < n` is not present, since for `n = 0`, both sides are satisfied;
the right-hand side holds, since `padicValNat q 0 = 0` by definition.) -/
theorem eq_sq_add_sq_iff {n : ℕ} :
(∃ x y : ℕ, n = x ^ 2 + y ^ 2) ↔ ∀ {q : ℕ}, q.Prime → q % 4 = 3 → Even (padicValNat q n) :=
by
rcases n.eq_zero_or_pos with (rfl | hn₀)
·
exact
⟨fun _ q _ _ => (@padicValNat.zero q).symm ▸ Even.zero, fun _ => ⟨0, 0, rfl⟩⟩
-- now `0 < n`
rw [Nat.eq_sq_add_sq_iff_eq_sq_mul]
refine ⟨fun H q hq h => ?_, fun H => ?_⟩
· obtain ⟨a, b, h₁, h₂⟩ := H
have hqb := padicValNat.eq_zero_of_not_dvd fun hf => (hq.mod_four_ne_three_of_dvd_isSquare_neg_one hf h₂) h
have hab : a ^ 2 * b ≠ 0 := h₁ ▸ hn₀.ne'
have ha₂ := left_ne_zero_of_mul hab
have ha := mt sq_eq_zero_iff.mpr ha₂
have hb := right_ne_zero_of_mul hab
haveI hqi : Fact q.Prime := ⟨hq⟩
simp_rw [h₁, padicValNat.mul ha₂ hb, padicValNat.pow 2 ha, hqb, add_zero]
exact even_two_mul _
· obtain ⟨b, a, hb₀, ha₀, hab, hb⟩ := Nat.sq_mul_squarefree_of_pos hn₀
refine ⟨a, b, hab.symm, (ZMod.isSquare_neg_one_iff hb).mpr fun {q} hqp hqb hq4 => ?_⟩
refine Nat.not_even_iff_odd.2 ?_ (H hqp hq4)
have hqb' : padicValNat q b = 1 :=
b.factorization_def hqp ▸
le_antisymm (hb.natFactorization_le_one _) ((hqp.dvd_iff_one_le_factorization hb₀.ne').mp hqb)
haveI hqi : Fact q.Prime := ⟨hqp⟩
simp_rw [← hab, padicValNat.mul (pow_ne_zero 2 ha₀.ne') hb₀.ne', hqb', padicValNat.pow 2 ha₀.ne']
exact odd_two_mul_add_one _
