A Liouville inequality through the resultant: |Res(F, G)| is controlled by max(|F(θ)|, |G(θ)|)

import Mathlib

namespace Transcendence

/-- A Liouville inequality through the resultant.

Let `F, G ∈ ℂ[X]` have Mahler measures at least `1`. Then at every point `θ`,
`|Res(F, G)| ≤ 2^(deg F · deg G) · M(F)^(deg G) · M(G)^(deg F) · max(|F(θ)|, |G(θ)|)`.

Let `α₁` be the root of `F` or `G` nearest to `θ`, say a root of `F`. Writing the resultant as
`a^(deg G) ∏ G(α)` over the roots `α` of `F`, the factor `G(α₁)` is at most `2^(deg G) |G(θ)|`,
because every root `β` of `G` has `|α₁ - β| ≤ 2 |θ - β|`, and each other factor `G(α)` is at most
`2^(deg G) max(1, |α|)^(deg G) M(G)`. If neither polynomial has a root, both are constants and the
resultant is `1 ≤ M(F) = |F(θ)|`. This is the complex form of the inequality of Roy–Waldschmidt
(1997), Corollary 3.7, proved as in their Lemma 3.4: when `F, G ∈ ℤ[X]` are coprime, the resultant
is a non-zero integer and the right-hand side is at least `1`. -/
theorem norm_resultant_le_max_norm_eval (F G : Polynomial ℂ) (hF : 1 ≤ F.mahlerMeasure)
    (hG : 1 ≤ G.mahlerMeasure) (θ : ℂ) :
    ‖F.resultant G‖ ≤ 2 ^ (F.natDegree * G.natDegree) * F.mahlerMeasure ^ G.natDegree *
      G.mahlerMeasure ^ F.natDegree * max ‖F.eval θ‖ ‖G.eval θ‖ := by
  sorry

end Transcendence