Split families of Thue equations
DefinitionSplit Thue recurrence family#✓fully proved
Let \(d \in \mathbb{N}\), let \(G_i(n)\) be integers for \(i, n \in \mathbb{N}\), and let \(\gamma_i \in \mathbb{R}\) and \(\delta_i \in \mathbb{C}\) for \(i \in \mathbb{N}\). Then \((d, G, \gamma, \delta)\) is a split Thue recurrence family when \(d \ge 3\) and there are finite sets \(R_i \subseteq \mathbb{C}\) and complex numbers \(c_i(r)\) (\(i \in \mathbb{N}\), \(r \in \mathbb{C}\)) such that: for every \(1 \le i \le d\), \(c_i(r) \ne 0\) for all \(r \in R_i\), \(G_i(n) = \sum_{r \in R_i} c_i(r) r^n\) for all \(n\), \(\gamma_i \in R_i\), and \(|r| < \gamma_i\) for all \(r \in R_i\) with \(r \ne \gamma_i\); \(\gamma_1 \ge 0\), \(\gamma\) is strictly increasing on \(\{1, \dots, d - 1\}\), and \(\gamma_{d-1} = \gamma_d\); \(c_{d-1}(\gamma_{d-1}) = c_d(\gamma_d)\); for \(i \in \{d - 1, d\}\), \(\delta_i \in R_i\), \(\delta_i \ne \gamma_i\), and \(|r| < |\delta_i|\) for all \(r \in R_i\) other than \(\gamma_i\) and \(\delta_i\); and \(|\delta_{d-1}| < |\delta_d| < \gamma_{d-2}\) and \(\gamma_{d-2}^2 < \gamma_d |\delta_d|\).
In words: each \(G_i\) is a simple linear recurrence with dominant root \(\gamma_i\), the sequences \(G_{d-1}\) and \(G_d\) share their dominant root and its coefficient, and \(\delta_{d-1}\), \(\delta_d\) are their second dominant roots.
public def IsSplitThueRecurrenceFamily (d : ℕ) (G : ℕ → ℕ → ℤ) (γ : ℕ → ℝ) (δ : ℕ → ℂ) :
Prop :=
3 ≤ d ∧ ∃ (R : ℕ → Finset ℂ) (c : ℕ → ℂ → ℂ),
(∀ i ∈ Finset.Icc 1 d, (∀ r ∈ R i, c i r ≠ 0) ∧
∀ n, (G i n : ℂ) = ∑ r ∈ R i, c i r * r ^ n) ∧
(∀ i ∈ Finset.Icc 1 d, ((γ i : ℝ) : ℂ) ∈ R i ∧ ∀ r ∈ R i, r ≠ γ i → ‖r‖ < γ i) ∧
0 ≤ γ 1 ∧ StrictMonoOn γ (Set.Icc 1 (d - 1)) ∧ γ (d - 1) = γ d ∧
c (d - 1) (γ (d - 1)) = c d (γ d) ∧
(∀ i ∈ ({d - 1, d} : Finset ℕ), δ i ∈ R i ∧ δ i ≠ γ i ∧
∀ r ∈ R i, r ≠ γ i → r ≠ δ i → ‖r‖ < ‖δ i‖) ∧
‖δ (d - 1)‖ < ‖δ d‖ ∧ ‖δ d‖ < γ (d - 2) ∧ γ (d - 2) ^ 2 < γ d * ‖δ d‖
Sources
- Tobias Hilgart, On Split Families of Thue Equations with Linear Recurrence Sequences as Factors, INTEGERS 25 (2025), Article A35, Theorem 1 (conditions 1-3); dominant roots taken real and nonnegative as in the paper's standing assumption after Corollary 1.
Used by 7
TheoremA split Thue recurrence family has at least three sequences#✓fully proved
If \((d, G, \gamma, \delta)\) is a split Thue recurrence family, then \(d \ge 3\).
public theorem IsSplitThueRecurrenceFamily.three_le {d : ℕ} {G : ℕ → ℕ → ℤ} {γ : ℕ → ℝ}
{δ : ℕ → ℂ} (h : IsSplitThueRecurrenceFamily d G γ δ) : 3 ≤ d
public def IsSplitThueRecurrenceFamily (d : ℕ) (G : ℕ → ℕ → ℤ) (γ : ℕ → ℝ) (δ : ℕ → ℂ) :
Prop :=
3 ≤ d ∧ ∃ (R : ℕ → Finset ℂ) (c : ℕ → ℂ → ℂ),
(∀ i ∈ Finset.Icc 1 d, (∀ r ∈ R i, c i r ≠ 0) ∧
∀ n, (G i n : ℂ) = ∑ r ∈ R i, c i r * r ^ n) ∧
(∀ i ∈ Finset.Icc 1 d, ((γ i : ℝ) : ℂ) ∈ R i ∧ ∀ r ∈ R i, r ≠ γ i → ‖r‖ < γ i) ∧
0 ≤ γ 1 ∧ StrictMonoOn γ (Set.Icc 1 (d - 1)) ∧ γ (d - 1) = γ d ∧
c (d - 1) (γ (d - 1)) = c d (γ d) ∧
(∀ i ∈ ({d - 1, d} : Finset ℕ), δ i ∈ R i ∧ δ i ≠ γ i ∧
∀ r ∈ R i, r ≠ γ i → r ≠ δ i → ‖r‖ < ‖δ i‖) ∧
‖δ (d - 1)‖ < ‖δ d‖ ∧ ‖δ d‖ < γ (d - 2) ∧ γ (d - 2) ^ 2 < γ d * ‖δ d‖
WantedExt/NumberTheory/SplitThueRecurrenceWanted.lean:47
Sources
- Tobias Hilgart, On Split Families of Thue Equations with Linear Recurrence Sequences as Factors, INTEGERS 25 (2025), Article A35, Theorem 1 (the conditions mention
γ (d - 2)).
Uses 1
TheoremExample of a split Thue recurrence family#✓fully proved
Let \(G_1(n) = 3^n\), \(G_2(n) = 5^n + 1\) and \(G_i(n) = 5^n + 2^n\) for \(i \notin \{1, 2\}\); let \(\gamma_1 = 3\) and \(\gamma_i = 5\) for \(i \ne 1\); and let \(\delta_2 = 1\) and \(\delta_i = 2\) for \(i \ne 2\). Then \((3, G, \gamma, \delta)\) is a split Thue recurrence family: the dominant roots of \(G_1, G_2, G_3\) are \(3, 5, 5\) and the second dominant roots of \(G_2, G_3\) are \(1, 2\).
public theorem isSplitThueRecurrenceFamily_example :
IsSplitThueRecurrenceFamily 3
(fun i n => if i = 1 then 3 ^ n else if i = 2 then 5 ^ n + 1 else 5 ^ n + 2 ^ n)
(fun i => if i = 1 then 3 else 5) (fun i => if i = 2 then 1 else 2)
public def IsSplitThueRecurrenceFamily (d : ℕ) (G : ℕ → ℕ → ℤ) (γ : ℕ → ℝ) (δ : ℕ → ℂ) :
Prop :=
3 ≤ d ∧ ∃ (R : ℕ → Finset ℂ) (c : ℕ → ℂ → ℂ),
(∀ i ∈ Finset.Icc 1 d, (∀ r ∈ R i, c i r ≠ 0) ∧
∀ n, (G i n : ℂ) = ∑ r ∈ R i, c i r * r ^ n) ∧
(∀ i ∈ Finset.Icc 1 d, ((γ i : ℝ) : ℂ) ∈ R i ∧ ∀ r ∈ R i, r ≠ γ i → ‖r‖ < γ i) ∧
0 ≤ γ 1 ∧ StrictMonoOn γ (Set.Icc 1 (d - 1)) ∧ γ (d - 1) = γ d ∧
c (d - 1) (γ (d - 1)) = c d (γ d) ∧
(∀ i ∈ ({d - 1, d} : Finset ℕ), δ i ∈ R i ∧ δ i ≠ γ i ∧
∀ r ∈ R i, r ≠ γ i → r ≠ δ i → ‖r‖ < ‖δ i‖) ∧
‖δ (d - 1)‖ < ‖δ d‖ ∧ ‖δ d‖ < γ (d - 2) ∧ γ (d - 2) ^ 2 < γ d * ‖δ d‖
WantedExt/NumberTheory/SplitThueRecurrenceWanted.lean:47
Sources
- Tobias Hilgart, On Split Families of Thue Equations with Linear Recurrence Sequences as Factors, INTEGERS 25 (2025), Article A35, Theorem 1 (conditions 1-3).
Uses 1
TheoremHilgart's theorem on split families of Thue equations#●ready to prove
Let \((d, G, \gamma, \delta)\) be a split Thue recurrence family. Then there is \(\kappa \in \mathbb{R}\) such that for every \(n \in \mathbb{N}\) and all integers \(x, y\) with \(|y| \ge 2\) and
we have \(\log |x| \le \kappa\), \(\log |y| \le \kappa\) and \(n \le \kappa\) (where \(\log 0 = 0\)).
public theorem_wanted splitThue_recurrence_solutions_bounded {d : ℕ} {G : ℕ → ℕ → ℤ}
{γ : ℕ → ℝ} {δ : ℕ → ℂ} (hF : IsSplitThueRecurrenceFamily d G γ δ) :
∃ κ : ℝ, ∀ (n : ℕ) (x y : ℤ), 2 ≤ |y| →
((∏ i ∈ Finset.Icc 1 d, (x - G i n * y)) - y ^ d = 1 ∨
(∏ i ∈ Finset.Icc 1 d, (x - G i n * y)) - y ^ d = -1) →
Real.log |(x : ℝ)| ≤ κ ∧ Real.log |(y : ℝ)| ≤ κ ∧ (n : ℝ) ≤ κ
public def IsSplitThueRecurrenceFamily (d : ℕ) (G : ℕ → ℕ → ℤ) (γ : ℕ → ℝ) (δ : ℕ → ℂ) :
Prop :=
3 ≤ d ∧ ∃ (R : ℕ → Finset ℂ) (c : ℕ → ℂ → ℂ),
(∀ i ∈ Finset.Icc 1 d, (∀ r ∈ R i, c i r ≠ 0) ∧
∀ n, (G i n : ℂ) = ∑ r ∈ R i, c i r * r ^ n) ∧
(∀ i ∈ Finset.Icc 1 d, ((γ i : ℝ) : ℂ) ∈ R i ∧ ∀ r ∈ R i, r ≠ γ i → ‖r‖ < γ i) ∧
0 ≤ γ 1 ∧ StrictMonoOn γ (Set.Icc 1 (d - 1)) ∧ γ (d - 1) = γ d ∧
c (d - 1) (γ (d - 1)) = c d (γ d) ∧
(∀ i ∈ ({d - 1, d} : Finset ℕ), δ i ∈ R i ∧ δ i ≠ γ i ∧
∀ r ∈ R i, r ≠ γ i → r ≠ δ i → ‖r‖ < ‖δ i‖) ∧
‖δ (d - 1)‖ < ‖δ d‖ ∧ ‖δ d‖ < γ (d - 2) ∧ γ (d - 2) ^ 2 < γ d * ‖δ d‖
WantedExt/NumberTheory/SplitThueRecurrenceWanted.lean:47
Sources
- Tobias Hilgart, On Split Families of Thue Equations with Linear Recurrence Sequences as Factors, INTEGERS 25 (2025), Article A35, Theorem 1. The computability of
κis not recorded.
Uses 1
TheoremSplit Thue families eventually have only trivial solutions#●ready to prove
Let \((d, G, \gamma, \delta)\) be a split Thue recurrence family. Then there is \(n_0\) such that for every \(n \ge n_0\) and all integers \(x, y\),
holds if and only if \((x, y) = (\pm 1, 0)\) or, for some \(1 \le i \le d\), \((x, y) = (G_i(n), 1)\) or \((x, y) = (-G_i(n), -1)\).
public theorem_wanted splitThue_recurrence_solutions_eventually_trivial {d : ℕ}
{G : ℕ → ℕ → ℤ} {γ : ℕ → ℝ} {δ : ℕ → ℂ} (hF : IsSplitThueRecurrenceFamily d G γ δ) :
∃ n₀ : ℕ, ∀ n ≥ n₀, ∀ x y : ℤ,
((∏ i ∈ Finset.Icc 1 d, (x - G i n * y)) - y ^ d = 1 ∨
(∏ i ∈ Finset.Icc 1 d, (x - G i n * y)) - y ^ d = -1) ↔
((x = 1 ∨ x = -1) ∧ y = 0) ∨
∃ i ∈ Finset.Icc 1 d, (x = G i n ∧ y = 1) ∨ (x = -G i n ∧ y = -1)
public def IsSplitThueRecurrenceFamily (d : ℕ) (G : ℕ → ℕ → ℤ) (γ : ℕ → ℝ) (δ : ℕ → ℂ) :
Prop :=
3 ≤ d ∧ ∃ (R : ℕ → Finset ℂ) (c : ℕ → ℂ → ℂ),
(∀ i ∈ Finset.Icc 1 d, (∀ r ∈ R i, c i r ≠ 0) ∧
∀ n, (G i n : ℂ) = ∑ r ∈ R i, c i r * r ^ n) ∧
(∀ i ∈ Finset.Icc 1 d, ((γ i : ℝ) : ℂ) ∈ R i ∧ ∀ r ∈ R i, r ≠ γ i → ‖r‖ < γ i) ∧
0 ≤ γ 1 ∧ StrictMonoOn γ (Set.Icc 1 (d - 1)) ∧ γ (d - 1) = γ d ∧
c (d - 1) (γ (d - 1)) = c d (γ d) ∧
(∀ i ∈ ({d - 1, d} : Finset ℕ), δ i ∈ R i ∧ δ i ≠ γ i ∧
∀ r ∈ R i, r ≠ γ i → r ≠ δ i → ‖r‖ < ‖δ i‖) ∧
‖δ (d - 1)‖ < ‖δ d‖ ∧ ‖δ d‖ < γ (d - 2) ∧ γ (d - 2) ^ 2 < γ d * ‖δ d‖
WantedExt/NumberTheory/SplitThueRecurrenceWanted.lean:47
Sources
- Tobias Hilgart, On Split Families of Thue Equations with Linear Recurrence Sequences as Factors, INTEGERS 25 (2025), Article A35, Corollary 1. The computability of
n₀is not recorded.
Uses 1
TheoremAsymptotics of the roots of a split Thue family#●ready to prove
Let \((d, G, \gamma, \delta)\) be a split Thue recurrence family. Call reals \(\alpha_i(n)\) (\(i, n \in \mathbb{N}\)) an admissible labelling if there is \(N\) such that for all \(n \ge N\) and \(1 \le i \le d\), \(\prod_{k=1}^{d} (\alpha_i(n) - G_k(n)) = 1\) and \(|\alpha_i(n) - G_i(n)| < 1\). Then, first, there is \(N\) such that for all \(n \ge N\) every \(z \in \mathbb{C}\) with \(\prod_{k=1}^{d} (z - G_k(n)) = 1\) is real; second, an admissible labelling exists; third, for every admissible labelling \(\alpha\) and every \(1 \le i \le d\) there are \(C \in \mathbb{R}\) and \(N\) such that for all \(n \ge N\)
where the product is over \(1 \le k \le d\) with \(k \ne i\), and \(\Gamma_i = \gamma_i^{i-1} (\prod_{k=i+1}^{d-2} \gamma_k) \gamma_d^2\) if \(i \le d - 2\) and \(\Gamma_i = \gamma_d^{d-2} |\delta_d|\) otherwise.
public theorem_wanted splitThue_recurrence_roots_asymptotic {d : ℕ} {G : ℕ → ℕ → ℤ}
{γ : ℕ → ℝ} {δ : ℕ → ℂ} (hF : IsSplitThueRecurrenceFamily d G γ δ) :
(∃ N : ℕ, ∀ n ≥ N, ∀ z : ℂ, ∏ k ∈ Finset.Icc 1 d, (z - G k n) = 1 → z.im = 0) ∧
(∃ α : ℕ → ℕ → ℝ, ∃ N : ℕ, ∀ n ≥ N, ∀ i ∈ Finset.Icc 1 d,
∏ k ∈ Finset.Icc 1 d, (α n i - G k n) = 1 ∧ |α n i - G i n| < 1) ∧
∀ α : ℕ → ℕ → ℝ, (∃ N : ℕ, ∀ n ≥ N, ∀ i ∈ Finset.Icc 1 d,
∏ k ∈ Finset.Icc 1 d, (α n i - G k n) = 1 ∧ |α n i - G i n| < 1) →
∀ i ∈ Finset.Icc 1 d, ∃ (C : ℝ) (N : ℕ), ∀ n ≥ N,
|(α n i - G i n) * ∏ k ∈ (Finset.Icc 1 d).erase i, ((G i n : ℝ) - G k n) - 1| ≤
C * ((if i ≤ d - 2 then γ i ^ (i - 1) * (∏ k ∈ Finset.Icc (i + 1) (d - 2), γ k) *
γ d ^ 2 else γ d ^ (d - 2) * ‖δ d‖)⁻¹) ^ n
public def IsSplitThueRecurrenceFamily (d : ℕ) (G : ℕ → ℕ → ℤ) (γ : ℕ → ℝ) (δ : ℕ → ℂ) :
Prop :=
3 ≤ d ∧ ∃ (R : ℕ → Finset ℂ) (c : ℕ → ℂ → ℂ),
(∀ i ∈ Finset.Icc 1 d, (∀ r ∈ R i, c i r ≠ 0) ∧
∀ n, (G i n : ℂ) = ∑ r ∈ R i, c i r * r ^ n) ∧
(∀ i ∈ Finset.Icc 1 d, ((γ i : ℝ) : ℂ) ∈ R i ∧ ∀ r ∈ R i, r ≠ γ i → ‖r‖ < γ i) ∧
0 ≤ γ 1 ∧ StrictMonoOn γ (Set.Icc 1 (d - 1)) ∧ γ (d - 1) = γ d ∧
c (d - 1) (γ (d - 1)) = c d (γ d) ∧
(∀ i ∈ ({d - 1, d} : Finset ℕ), δ i ∈ R i ∧ δ i ≠ γ i ∧
∀ r ∈ R i, r ≠ γ i → r ≠ δ i → ‖r‖ < ‖δ i‖) ∧
‖δ (d - 1)‖ < ‖δ d‖ ∧ ‖δ d‖ < γ (d - 2) ∧ γ (d - 2) ^ 2 < γ d * ‖δ d‖
WantedExt/NumberTheory/SplitThueRecurrenceWanted.lean:47
Sources
- Tobias Hilgart, On Split Families of Thue Equations with Linear Recurrence Sequences as Factors, INTEGERS 25 (2025), Article A35, Lemma 1. The
O-term is written as|(α⁽ⁱ⁾ - G i n) * ∏_{k ≠ i} (G i n - G k n) - 1| ≤ C * γ_ε⁻ⁿ;δ denters through its modulus.
Uses 1
TheoremGrowth of the roots of a split Thue family#●ready to prove
Let \((d, G, \gamma, \delta)\) be a split Thue recurrence family, and let \(\alpha_i(n)\) (\(i, n \in \mathbb{N}\)) be reals for which there is \(N\) such that for all \(n \ge N\) and \(1 \le i \le d\), \(\prod_{k=1}^{d} (\alpha_i(n) - G_k(n)) = 1\) and \(|\alpha_i(n) - G_i(n)| < 1\). Then there are \(c > 0\) and \(N'\) such that for all \(n \ge N'\) and \(1 \le i \le d\) we have \(|\alpha_i(n)| \ge c \gamma_i^n\), and for every \(1 \le j \le d\) with \(j \ne i\) both \(|\alpha_i(n) - \alpha_j(n)|\) and \(|\alpha_i(n) - G_j(n)|\) are at least \(c |\delta_d|^n\) if \(\{i, j\} = \{d - 1, d\}\), and at least \(c \max(\gamma_i, \gamma_j)^n\) otherwise.
public theorem_wanted splitThue_recurrence_roots_growth {d : ℕ} {G : ℕ → ℕ → ℤ}
{γ : ℕ → ℝ} {δ : ℕ → ℂ} (hF : IsSplitThueRecurrenceFamily d G γ δ)
(α : ℕ → ℕ → ℝ) (hα : ∃ N : ℕ, ∀ n ≥ N, ∀ i ∈ Finset.Icc 1 d,
∏ k ∈ Finset.Icc 1 d, (α n i - G k n) = 1 ∧ |α n i - G i n| < 1) :
∃ c > 0, ∃ N : ℕ, ∀ n ≥ N, ∀ i ∈ Finset.Icc 1 d,
c * γ i ^ n ≤ |α n i| ∧ ∀ j ∈ Finset.Icc 1 d, j ≠ i →
(({i, j} : Finset ℕ) = {d - 1, d} →
c * ‖δ d‖ ^ n ≤ |α n i - α n j| ∧ c * ‖δ d‖ ^ n ≤ |α n i - G j n|) ∧
(({i, j} : Finset ℕ) ≠ {d - 1, d} →
c * max (γ i) (γ j) ^ n ≤ |α n i - α n j| ∧
c * max (γ i) (γ j) ^ n ≤ |α n i - G j n|)
public def IsSplitThueRecurrenceFamily (d : ℕ) (G : ℕ → ℕ → ℤ) (γ : ℕ → ℝ) (δ : ℕ → ℂ) :
Prop :=
3 ≤ d ∧ ∃ (R : ℕ → Finset ℂ) (c : ℕ → ℂ → ℂ),
(∀ i ∈ Finset.Icc 1 d, (∀ r ∈ R i, c i r ≠ 0) ∧
∀ n, (G i n : ℂ) = ∑ r ∈ R i, c i r * r ^ n) ∧
(∀ i ∈ Finset.Icc 1 d, ((γ i : ℝ) : ℂ) ∈ R i ∧ ∀ r ∈ R i, r ≠ γ i → ‖r‖ < γ i) ∧
0 ≤ γ 1 ∧ StrictMonoOn γ (Set.Icc 1 (d - 1)) ∧ γ (d - 1) = γ d ∧
c (d - 1) (γ (d - 1)) = c d (γ d) ∧
(∀ i ∈ ({d - 1, d} : Finset ℕ), δ i ∈ R i ∧ δ i ≠ γ i ∧
∀ r ∈ R i, r ≠ γ i → r ≠ δ i → ‖r‖ < ‖δ i‖) ∧
‖δ (d - 1)‖ < ‖δ d‖ ∧ ‖δ d‖ < γ (d - 2) ∧ γ (d - 2) ^ 2 < γ d * ‖δ d‖
WantedExt/NumberTheory/SplitThueRecurrenceWanted.lean:47
Sources
- Tobias Hilgart, On Split Families of Thue Equations with Linear Recurrence Sequences as Factors, INTEGERS 25 (2025), Article A35, Lemma 2, including its last sentence (the same bounds with
α⁽ʲ⁾replaced byG j n).Ωis the paper's lower bound|f n| ≥ c * g nfor largen.
Uses 1
TheoremDeterminants of logarithms in a split Thue family#●ready to prove
Let \((d, G, \gamma, \delta)\) be a split Thue recurrence family, let \(\alpha_i(n)\) (\(i, n \in \mathbb{N}\)) be reals for which there is \(N\) such that for all \(n \ge N\) and \(1 \le i \le d\), \(\prod_{l=1}^{d} (\alpha_i(n) - G_l(n)) = 1\) and \(|\alpha_i(n) - G_i(n)| < 1\), and let \(1 \le k \le d - 1\). Let \(B_k(n)\) be the \(k \times k\) matrix with entries \(\log |\alpha_i(n) - G_j(n)|\) for \(1 \le i, j \le k\), where \(\log 0 = 0\). Then there are \(c_1 > 0\), \(c_2 > 0\) and \(N'\) such that \(c_1 n^k \le |\det B_k(n)| \le c_2 n^k\) for all \(n \ge N'\).
public theorem_wanted splitThue_recurrence_logUnitDet_asymptotic {d : ℕ} {G : ℕ → ℕ → ℤ}
{γ : ℕ → ℝ} {δ : ℕ → ℂ} (hF : IsSplitThueRecurrenceFamily d G γ δ)
(α : ℕ → ℕ → ℝ) (hα : ∃ N : ℕ, ∀ n ≥ N, ∀ i ∈ Finset.Icc 1 d,
∏ k ∈ Finset.Icc 1 d, (α n i - G k n) = 1 ∧ |α n i - G i n| < 1) (k : ℕ) (hk : 1 ≤ k) (hkd : k
≤ d - 1) :
∃ c₁ > 0, ∃ c₂ > 0, ∃ N : ℕ, ∀ n ≥ N,
c₁ * (n : ℝ) ^ k ≤
|(Matrix.of fun a b : Fin k => Real.log (α n ((a : ℕ) + 1) - G ((b : ℕ) + 1) n)).det| ∧
|(Matrix.of fun a b : Fin k => Real.log (α n ((a : ℕ) + 1) - G ((b : ℕ) + 1) n)).det| ≤
c₂ * (n : ℝ) ^ k
public def IsSplitThueRecurrenceFamily (d : ℕ) (G : ℕ → ℕ → ℤ) (γ : ℕ → ℝ) (δ : ℕ → ℂ) :
Prop :=
3 ≤ d ∧ ∃ (R : ℕ → Finset ℂ) (c : ℕ → ℂ → ℂ),
(∀ i ∈ Finset.Icc 1 d, (∀ r ∈ R i, c i r ≠ 0) ∧
∀ n, (G i n : ℂ) = ∑ r ∈ R i, c i r * r ^ n) ∧
(∀ i ∈ Finset.Icc 1 d, ((γ i : ℝ) : ℂ) ∈ R i ∧ ∀ r ∈ R i, r ≠ γ i → ‖r‖ < γ i) ∧
0 ≤ γ 1 ∧ StrictMonoOn γ (Set.Icc 1 (d - 1)) ∧ γ (d - 1) = γ d ∧
c (d - 1) (γ (d - 1)) = c d (γ d) ∧
(∀ i ∈ ({d - 1, d} : Finset ℕ), δ i ∈ R i ∧ δ i ≠ γ i ∧
∀ r ∈ R i, r ≠ γ i → r ≠ δ i → ‖r‖ < ‖δ i‖) ∧
‖δ (d - 1)‖ < ‖δ d‖ ∧ ‖δ d‖ < γ (d - 2) ∧ γ (d - 2) ^ 2 < γ d * ‖δ d‖
WantedExt/NumberTheory/SplitThueRecurrenceWanted.lean:47
Sources
- Tobias Hilgart, On Split Families of Thue Equations with Linear Recurrence Sequences as Factors, INTEGERS 25 (2025), Article A35, Lemma 3.
Real.logis the logarithm of the absolute value;Θis the paper's two-sided boundc₁ n ^ k ≤ |det B_k| ≤ c₂ n ^ kfor largen.
Uses 1
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.