Transcendental

Results named in Tau Ceti's TauCeti.NumberTheory.Transcendental modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremBaker's denominator bound #

If each of 1, …, k divides the integer L, then for every integer x and all l, m,

L ^ m Δ(x; k, l, m) = L ^ m (1 / m!) (d / dx) ^ m (Δ(x; k) ^ l)

is an integer.

TauCeti.pow_mul_eval_hasseDeriv_multichoose_X_add_one_pow_mem_range_intCast {k : ℕ} {L : ℤ}
  (hL : ∀ j ∈ Finset.Icc 1 k, ↑j ∣ L) (l m : ℕ) (x : ℤ) :
  ↑L ^ m *
      Polynomial.eval (↑x) ((Polynomial.hasseDeriv m) (Ring.multichoose (Polynomial.X + 1) k ^ l)) ∈
    Set.range Int.cast

Lean

Formalized in Tau Ceti as TauCeti.pow_mul_eval_hasseDeriv_multichoose_X_add_one_pow_mem_range_intCast.

Other forms

Baker's denominator bound, classical form. Formalized in Tau Ceti as TauCeti.lcm_pow_mul_eval_hasseDeriv_multichoose_X_add_one_pow_mem_range_intCast.

TauCeti.lcm_pow_mul_eval_hasseDeriv_multichoose_X_add_one_pow_mem_range_intCast (k l m : ℕ)
  (x : ℤ) :
  ↑((Finset.Icc 1 k).lcm id) ^ m *
      Polynomial.eval (↑x) ((Polynomial.hasseDeriv m) (Ring.multichoose (Polynomial.X + 1) k ^ l)) ∈
    Set.range Int.cast

Baker's denominator bound at points of a scaled lattice. Formalized in Tau Ceti as TauCeti.pow_mul_eval_hasseDeriv_map_multichoose_X_add_one_comp_C_mul_X_mem_range_intCast.

TauCeti.pow_mul_eval_hasseDeriv_map_multichoose_X_add_one_comp_C_mul_X_mem_range_intCast.{u_1}
  {K : Type u_1} [Field K] [CharZero K] {k : ℕ} {L : ℤ} (hL : ∀ j ∈ Finset.Icc 1 k, ↑j ∣ L) (q : ℤ)
  {x : K} (hx : ↑q * x ∈ Set.range Int.cast) (m : ℕ) :
  ↑L ^ m *
      Polynomial.eval x
        ((Polynomial.hasseDeriv m)
          (Polynomial.map (algebraMap ℚ K)
            ((Ring.multichoose (Polynomial.X + 1) k).comp (Polynomial.C ↑q * Polynomial.X)))) ∈
    Set.range Int.cast

Sources

LeanTauCeti.pow_mul_eval_hasseDeriv_multichoose_X_add_one_pow_mem_range_intCast · TauCeti.lcm_pow_mul_eval_hasseDeriv_multichoose_X_add_one_pow_mem_range_intCast · TauCeti.pow_mul_eval_hasseDeriv_map_multichoose_X_add_one_comp_C_mul_X_mem_range_intCast

TheoremThe Gelfond–Schneider theorem for real numbers (Evertse, Theorem 4.21)#

If α > 0 and β are real algebraic numbers with α ≠ 1 and β irrational, then α ^ β is transcendental.

TauCeti.transcendental_rpow {α β : ℝ} (hα : IsAlgebraic ℚ α) (hβ : IsAlgebraic ℚ β) (h0 : 0 < α)
  (h1 : α ≠ 1) (hirr : Irrational β) : Transcendental ℚ (α ^ β)

Lean

Formalized in Tau Ceti as TauCeti.transcendental_rpow.

Sources

LeanTauCeti.transcendental_rpow

Uses 4

Proof usesIterated Rolle's theorem · Liouville's inequality in exponential form · Schwarz's lemma for Schneider's auxiliary function · Siegel's lemma over a number field, with rational integer unknowns (Evertse, Theorem 3.20)

TheoremLiouville's lower bound for Gelfond's values (Karatarakis–Wiedijk, §3)#

Let K be a number field of degree h, α, β, γ ∈ K, m ∈ ℕ and c ∈ ℝ. There is c₂ ≥ 1 with the following property. Let q ^ 2 = 2 m n, r ≥ n and t₀ ≤ m, and let η_{ab} ∈ 𝓞 K, a, b < q, have house at most c ^ n n ^ ((n + 1) / 2), as for Gelfond's auxiliary function. If ρ = ∑_{a, b} η_{ab} ((a + 1) + (b + 1) β) ^ r α ^ ((a + 1) t₀) γ ^ ((b + 1) t₀) is nonzero, then 1 ≤ c₂ ^ r r ^ ((h - 1) r) |σ ρ| for every embedding σ : K →+* ℂ. In particular |σ ρ| ≥ c₂ ^ (-r) r ^ (-(h - 1) (r + 1)).

TauCeti.exists_one_le_pow_mul_norm_gelfond_value.{u_1} {K : Type u_1} [Field K] [NumberField K]
  (α β γ : K) (m : ℕ) (c : ℝ) :
  ∃ c₂,
    1 ≤ c₂ ∧
      ∀ (σ : K →+* ℂ) (n q r t₀ : ℕ) (η : Fin q → Fin q → NumberField.RingOfIntegers K),
        q ^ 2 = 2 * m * n →
          n ≤ r →
            t₀ ≤ m →
              (∀ (a b : Fin q), NumberField.house ↑(η a b) ≤ c ^ n * ↑n ^ ((↑n + 1) / 2)) →
                ∑ a,
                      ∑ b,
                        ↑(η a b) * (↑(↑a + 1) + ↑(↑b + 1) * β) ^ r *
                          (α ^ ((↑a + 1) * t₀) * γ ^ ((↑b + 1) * t₀)) ≠
                    0 →
                  1 ≤
                    c₂ ^ r * ↑r ^ ((Module.finrank ℚ K - 1) * r) *
                      ‖σ
                          (∑ a,
                            ∑ b,
                              ↑(η a b) * (↑(↑a + 1) + ↑(↑b + 1) * β) ^ r *
                                (α ^ ((↑a + 1) * t₀) * γ ^ ((↑b + 1) * t₀)))‖

Lean

Formalized in Tau Ceti as TauCeti.exists_one_le_pow_mul_norm_gelfond_value.

Sources

LeanTauCeti.exists_one_le_pow_mul_norm_gelfond_value

Uses 1

Proof usesLiouville's inequality in exponential form

TheoremSchwarz's lemma for Schneider's auxiliary function #

Let β ∈ ℂ be irrational and let F(z) = ∑_{i < D₁, j < D₂} a_{ij} z ^ i exp (j λ z) vanish at u + v β for 1 ≤ u, v ≤ L. If ‖a_{ij}‖ ≤ A, L (1 + ‖β‖) ≤ R, 3 R ≤ T and 1 ≤ T, then on the disc ‖z‖ ≤ R ‖F z‖ ≤ D₁ D₂ A T ^ D₁ exp (D₂ ‖λ‖ T) (3 R / T) ^ (L ^ 2).

TauCeti.norm_schneider_auxiliary_le {β : ℂ} (hβ : ∀ (q : ℚ), ↑q ≠ β) {l : ℂ} {L D₁ D₂ : ℕ}
  {a : Fin D₁ → Fin D₂ → ℂ} {A R T : ℝ} (ha : ∀ (i : Fin D₁) (j : Fin D₂), ‖a i j‖ ≤ A)
  (hzero :
    ∀ (u v : ℕ),
      1 ≤ u →
        u ≤ L →
          1 ≤ v →
            v ≤ L →
              ∑ i, ∑ j, a i j * (↑u + ↑v * β) ^ ↑i * Complex.exp (↑↑j * l * (↑u + ↑v * β)) = 0)
  (hR : ↑L * (1 + ‖β‖) ≤ R) (hRT : 3 * R ≤ T) (hT : 1 ≤ T) {z : ℂ} (hz : ‖z‖ ≤ R) :
  ‖∑ i, ∑ j, a i j * z ^ ↑i * Complex.exp (↑↑j * l * z)‖ ≤
    ↑D₁ * ↑D₂ * A * T ^ D₁ * Real.exp (↑D₂ * ‖l‖ * T) * (3 * R / T) ^ L ^ 2