transcendental — Mathlib

English

If x is a Liouville number, then x is transcendental over the integers; i.e., x is not a root of any nonzero polynomial with integer coefficients.

Русский

Если x является числом Лиувилля, то x трансцендентно над целыми; т.е. не является корнем никакого не нулевого многочлена с целыми коэффициентами.

LaTeX

$$$\\text{Liouville}(x)\\Rightarrow x \\text{ is transcendental over } \\mathbb Z,$$$

Lean4

/-- **Liouville's Theorem** -/
protected theorem transcendental {x : ℝ} (lx : Liouville x) : Transcendental ℤ x := by
  -- Proceed by contradiction: if `x` is algebraic, then `x` is the root (`ef0`) of a
    -- non-zero (`f0`) polynomial `f`

  rintro
    ⟨f : ℤ[X], f0, ef0⟩
        -- Change `aeval x f = 0` to `eval (map _ f) = 0`, who knew.

  replace ef0 : (f.map (algebraMap ℤ ℝ)).eval x = 0 := by rwa [aeval_def, ← eval_map] at ef0
  obtain ⟨A, hA, h⟩ :
    ∃ A : ℝ, 0 < A ∧ ∀ (a : ℤ) (b : ℕ), (1 : ℝ) ≤ ((b : ℝ) + 1) ^ f.natDegree * (|x - a / (b + 1)| * A) :=
    exists_pos_real_of_irrational_root lx.irrational f0 ef0
  rcases pow_unbounded_of_one_lt A (lt_add_one 1) with
    ⟨r, hn⟩
      -- Use the Liouville property, with exponent `r + deg f`.

  obtain ⟨a, b, b1, -, a1⟩ : ∃ a b : ℤ, 1 < b ∧ x ≠ a / b ∧ |x - a / b| < 1 / (b : ℝ) ^ (r + f.natDegree) :=
    lx (r + f.natDegree)
  have b0 : (0 : ℝ) < b :=
    zero_lt_one.trans
      (by rw [← Int.cast_one]; exact Int.cast_lt.mpr b1)
        -- Prove that `b ^ f.nat_degree * abs (x - a / b)` is strictly smaller than itself
          -- recall, this is a proof by contradiction!

  refine
    lt_irrefl ((b : ℝ) ^ f.natDegree * |x - ↑a / ↑b|)
      ?_
        -- clear denominators at `a1`

  rw [lt_div_iff₀' (pow_pos b0 _), pow_add, mul_assoc] at a1
  refine
    (?_ : (b : ℝ) ^ f.natDegree * |x - a / b| < 1 / A).trans_le
      ?_
        -- This branch of the proof uses the Liouville condition and the Archimedean property

  · refine (lt_div_iff₀' hA).mpr ?_
    refine lt_of_le_of_lt ?_ a1
    gcongr
    refine hn.le.trans ?_
    rw [one_add_one_eq_two]
    gcongr
    norm_cast
      -- this branch of the proof exploits the "integrality" of evaluations of polynomials
        -- at ratios of integers.

  · lift b to ℕ using zero_le_one.trans b1.le
    specialize h a b.pred
    rwa [← Nat.cast_succ, Nat.succ_pred_eq_of_pos (zero_lt_one.trans _), ← mul_assoc, ← div_le_iff₀ hA] at h
    exact Int.ofNat_lt.mp b1

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