Integer $s, t$

We explore $s$ and $t$ are positive integers.

Most statements here can be generalized to when $s/t$ are rationals, but the generalization will be deferred to homogeneity.

Main statements

• Φ is the discrete version of φ for integer $s$ and $t$.
• Φ_neg and Φ_rec characterize sequence Φ as generated by a recurrence relation.
• ΦFormula gives a formula for Φ as a finite sum over set ξSet.
• ΦAsymptotic shows the asymptotic behavior of Φ.
• dE_int_Asymptotic_coprime shows the asymptotic behavior of dE_int (integer version of dE) when $s$ and $t$ are coprime.
• w_Asymtotic_int shows the asymptotic behavior of wₗᵢ for integer $s$ and $t$.

When $s$ and $t$ are positive integers, Δ collaps to a subset of $l \cdot \gcd(s, t)$

theorem Δ_int (s t : ℕ+) : Δ ↑↑s ↑↑t ⊆ {δ : ℝ | ∃ (l : ℕ), δ = ↑l * ↑↑(s.gcd t)}

And obviously, all $δ$ are integers (natural numbers to be precise, but keeping it in ℤ simplifies some reasoning later).

We will also start creating the integer version of various objects we have created, starting with δnext_int.

theorem δlift (s t : ℕ+) (δ : ℝ) (mem : δ ∈ Δ ↑↑s ↑↑t) : ∃ (d : ℤ), ↑d = δ

theorem δnext_int (s t : ℕ+) (δ : ℤ) : ∃ (d' : ℤ), ↑d' = δnext ↑↑s ↑↑t ↑δ

Since δ are all integers, their gaps is at least 1.

theorem δnext_int_larger (s t : ℕ+) (δ : ℤ) : δnext ↑↑s ↑↑t ↑δ ≥ ↑δ + 1

We can now define integer versions of δₖ.

noncomputable def δₖ_int (s t : ℕ+) : ℕ → ℤ

Equations

• δₖ_int s t 0 = 0
• δₖ_int s t k.succ = Classical.choose ⋯

theorem δₖ_int_agree (s t : ℕ+) (k : ℕ) : ↑(δₖ_int s t k) = δₖ (↑↑s) (↑↑t) k

noncomputable def Jline_int (s t : ℕ+) (δ : ℤ) : ℕ

Equations

• Jline_int s t δ = Jline ↑↑s ↑↑t ↑δ

theorem Jline_int_rec (s t : ℕ+) (δ : ℤ) (d0 : δ ≠ 0) : Jline_int s t δ = Jline_int s t (δ - ↑↑s) + Jline_int s t (δ - ↑↑t)

noncomputable def Jceiled_int (s t : ℕ+) (δ : ℤ) : ℕ

Equations

• Jceiled_int s t δ = Jceiled ↑↑s ↑↑t ↑δ

theorem Jceiled_int_accum (s t : ℕ+) (δ : ℤ) : Jceiled_int s t δ + Jline_int s t (δ + 1) = Jceiled_int s t (δ + 1)

And the integer version of dE.

noncomputable def dE_int (s t : ℕ+) : ℝ → ℤ

Equations

• dE_int s t n = match kₙ (↑↑s) (↑↑t) n with | some k => δₖ_int s t k | none => 0

theorem dE_int_agree (s t : ℕ+) (n : ℝ) : ↑(dE_int s t n) = dE (↑↑s) (↑↑t) n

theorem dE_int_homo (s t l : ℕ+) (n : ℝ) : ↑↑l * dE_int s t n = dE_int (l * s) (l * t) n

Let's introduce a new sequence Φ(δ) that's simply Jceiled_int shifted by 1.

noncomputable def Φ (s t : ℕ+) (δ : ℤ) : ℕ

Equations

• Φ s t δ = 1 + Jceiled_int s t δ

theorem Φ_agree (s t : ℕ+) (δ : ℤ) : Φ s t δ = φ ↑↑s ↑↑t ↑δ

theorem Φ_mono (s t : ℕ+) : Monotone (Φ s t)

theorem Φ_pos (s t : ℕ+) (δ : ℤ) : 0 < Φ s t δ

theorem Φ_symm (s t : ℕ+) (δ : ℤ) : Φ s t δ = Φ t s δ

Φ(δ) is the unique sequence that satisfies the following conditions:

• Φ(< 0) = 1
• Φ(δ ≥ 0) = Φ(δ - s) + Φ(δ - t) As an example, for $s = 1$ and $t = 2$, this is the Fibonacci sequence (shifted in index).

theorem Φ_neg (s t : ℕ+) (δ : ℤ) (dpos : δ < 0) : Φ s t δ = 1

theorem Φ_rec (s t : ℕ+) (δ : ℤ) (dpos : δ ≥ 0) : Φ s t δ = Φ s t (δ - ↑↑s) + Φ s t (δ - ↑↑t)

Φ is the discrete analog of the continuous function φ.

def ΔceiledByΦ (s t : ℕ+) (n : ℝ) : Set ℤ

Equations

• ΔceiledByΦ s t n = {δ : ℤ | ↑(Φ s t δ) ≤ n}

theorem ΔceiledByΦ_agree (s t : ℕ+) (n : ℝ) : Int.cast '' ΔceiledByΦ s t n = δceiledByφ (↑↑s) (↑↑t) n ∩ Int.cast '' Set.univ

theorem dE_int_range_agree (s t : ℕ+) (n : ℝ) : Int.cast '' Set.Iic (dE_int s t n - 1) = Set.Iio (dE (↑↑s) (↑↑t) n) ∩ Int.cast '' Set.univ

And finally, we show that Φ is the inverse function of dE_int in some sense.

theorem Φ_inv (s t : ℕ+) (n : ℝ) (n1 : n ≥ 1) : ΔceiledByΦ s t n = Set.Iic (dE_int s t n - 1)

theorem Φδₖ (s t : ℕ+) (k : ℕ) : Φ s t (δₖ_int s t k) = nₖ (↑↑s) (↑↑t) (k + 1)

theorem Φδₖt (s t : ℕ+) (k : ℕ) : Φ s t (δₖ_int s t k - ↑↑t) = wₖ (↑↑s) (↑↑t) (k + 1)

Analog to φδₖ, Φ sends δₖ back to nₖ. But since Φ is discrete, we can develop another theorem: when Φ changes, it precisely correspond to when nₖ move to the next value.

theorem Φjump (s t : ℕ+) (δ : ℤ) (k : ℕ) (h : Φ s t δ = nₖ (↑↑s) (↑↑t) k) (hlt : Φ s t δ < Φ s t (δ + 1)) : Φ s t (δ + 1) = nₖ (↑↑s) (↑↑t) (k + 1)

We will investigate the generator function $Z\{Φ\}(x) = \sum_{i\inℕ} Φ(i) x^i$ and and show that it converges to a nice function.

theorem ΛexchangeMem (s t : ℕ+) (pq : ℕ × ℕ) (i : ℕ) : pq ∈ (Λceiled ↑↑s ↑↑t ↑(i + pq.1 * ↑s + pq.2 * ↑t)).toFinset

def Λexchange (s t : ℕ+) : (ℕ × ℕ) × ℕ ≃ (i : ℕ) × { x : ℕ × ℕ // x ∈ (Λceiled ↑↑s ↑↑t ↑i).toFinset }

Equations

• One or more equations did not get rendered due to their size.

We will relate Φ with this polynomial.

noncomputable def ξPolynomial (s t : ℕ+) : Polynomial ℂ

Equations

• ξPolynomial s t = (Polynomial.monomial ↑s) 1 + (Polynomial.monomial ↑t) 1 - Polynomial.C 1

theorem ξPolynomialDerivative (s t : ℕ+) : Polynomial.derivative (ξPolynomial s t) = (Polynomial.monomial (↑s - 1)) ↑↑s + (Polynomial.monomial (↑t - 1)) ↑↑t

theorem ξPolynomialNonzero (s t : ℕ+) : ξPolynomial s t ≠ 0

theorem ξPolynomialFactorizeMulti (s t : ℕ+) : ξPolynomial s t = Polynomial.C (ξPolynomial s t).leadingCoeff * (Multiset.map (fun (x : ℂ) => Polynomial.X - Polynomial.C x) (ξPolynomial s t).roots).prod

Φ will be expanded in terms of ξSet, the roots of ξPolynomial. We also show ξPolynomial doesn't have multiple root and has simple factorization over ξSet.

noncomputable def ξSet (s t : ℕ+) : Finset ℂ

Equations

• ξSet s t = (ξPolynomial s t).roots.toFinset

theorem ξNonMult (s t : ℕ+) (r : ℂ) (rmem : r ∈ ξSet s t) : ↑↑s * r ^ (↑s - 1) + ↑↑t * r ^ (↑t - 1) ≠ 0

theorem ξPolynomialSeparable (s t : ℕ+) : (ξPolynomial s t).Separable

theorem ξPolynomialFactorize (s t : ℕ+) : ξPolynomial s t = Polynomial.C (ξPolynomial s t).leadingCoeff * Lagrange.nodal (ξSet s t) id

The generating function Z{Φ}(x) converges to a rational function. The bound here is not sharp, but it should be sufficient for future reasoning over complex plane.

theorem ZΦ_sum (s t : ℕ+) (x : ℂ) (bound : ‖x‖ < 2⁻¹) : HasSum (fun (i : ℕ) => x ^ i * ↑(Φ s t ↑i)) (((Polynomial.eval 1 (ξPolynomial s t))⁻¹ - (Polynomial.eval x (ξPolynomial s t))⁻¹) * (1 - x)⁻¹)

theorem PartialFractionDecompostion {F : Type u_1} [Field F] [DecidableEq F] (x : F) (roots : Finset F) (hasroots : roots.Nonempty) (notroot : x ∉ roots) : (Polynomial.eval x (Lagrange.nodal roots id))⁻¹ = ∑ r ∈ roots, (x - r)⁻¹ * (Polynomial.eval r (Polynomial.derivative (Lagrange.nodal roots id)))⁻¹

theorem PartialFractionDecompostion2 {F : Type u_1} [Field F] [DecidableEq F] (x : F) (roots : Finset F) (coef : F) (hasroots : roots.Nonempty) (notroot : x ∉ roots) (not1 : x ≠ 1) (onenotroot : 1 ∉ roots) : ((Polynomial.eval 1 (Polynomial.C coef * Lagrange.nodal roots id))⁻¹ - (Polynomial.eval x (Polynomial.C coef * Lagrange.nodal roots id))⁻¹) * (1 - x)⁻¹ = ∑ r ∈ roots, (x - r)⁻¹ * (r - 1)⁻¹ * (Polynomial.eval r (Polynomial.derivative (Polynomial.C coef * Lagrange.nodal roots id)))⁻¹

theorem ΦX_sum_eq (s t : ℕ+) (x : ℂ) (bound : ‖x‖ < 2⁻¹) : ((Polynomial.eval 1 (ξPolynomial s t))⁻¹ - (Polynomial.eval x (ξPolynomial s t))⁻¹) * (1 - x)⁻¹ = ∑ ξ ∈ ξSet s t, (x - ξ)⁻¹ * (ξ - 1)⁻¹ * (↑↑s * ξ ^ (↑s - 1) + ↑↑t * ξ ^ (↑t - 1))⁻¹

theorem ZΦ_sum2 (s t : ℕ+) (x : ℂ) (bound : ‖x‖ < 2⁻¹) : HasSum (fun (i : ℕ) => x ^ i * ∑ ξ ∈ ξSet s t, ξ⁻¹ ^ i * (1 - ξ)⁻¹ * (↑↑s * ξ ^ ↑s + ↑↑t * ξ ^ ↑t)⁻¹) (((Polynomial.eval 1 (ξPolynomial s t))⁻¹ - (Polynomial.eval x (ξPolynomial s t))⁻¹) * (1 - x)⁻¹)

By inverting the transformation, we obtain a formula for Φ.

theorem ΦFormula (s t : ℕ+) (i : ℕ) : ↑(Φ s t ↑i) = ∑ ξ ∈ ξSet s t, ξ⁻¹ ^ i * (1 - ξ)⁻¹ * (↑↑s * ξ ^ ↑s + ↑↑t * ξ ^ ↑t)⁻¹

With formula for Φ developed, we further show one of the term in its summation is the "main" term that controls the growth rate, and use it to show the asymptotic behavior.

noncomputable def ξPolynomialℝ (s t : ℕ+) : Polynomial ℝ

Equations

• ξPolynomialℝ s t = (Polynomial.monomial ↑s) 1 + (Polynomial.monomial ↑t) 1 - Polynomial.C 1

theorem PowMono (a : ℕ+) : StrictMonoOn (fun (x : ℝ) => x ^ ↑a) (Set.Ici 0)

theorem ξPolynomialℝ_mono (s t : ℕ+) : StrictMonoOn (fun (x : ℝ) => Polynomial.eval x (ξPolynomialℝ s t)) (Set.Ici 0)

theorem ξPolynomialℝUniqueRoot (s t : ℕ+) : ∃! ξ : ℝ, ξ > 0 ∧ Polynomial.eval ξ (ξPolynomialℝ s t) = 0

ξ₀ Is the "main term" in ξSet. It is a real number between 0 and 1, and has the smallest norm among ξSet when $s$ an $t$ are coprime.

noncomputable def ξ₀ (s t : ℕ+) : ℝ

Equations

• ξ₀ s t = Exists.choose ⋯

theorem ξ₀min (s t : ℕ+) : ξ₀ s t > 0

theorem ξ₀max (s t : ℕ+) : ξ₀ s t < 1

theorem ξ₀eval (s t : ℕ+) : Polynomial.eval (ξ₀ s t) (ξPolynomialℝ s t) = 0

theorem ξ₀homo (s t l : ℕ+) : ξ₀ s t = ξ₀ (l * s) (l * t) ^ ↑l

theorem ξ₀Smallest (s t : ℕ+) (coprime : s.Coprime t) (ξ : ℂ) : ξ ∈ ξSet s t → ξ ≠ ↑(ξ₀ s t) → ξ₀ s t < ‖ξ‖

Res₀ is the coefficient associated to ξ₀.

noncomputable def Res₀ (s t : ℕ+) : ℝ

Equations

• Res₀ s t = (1 - ξ₀ s t) * (↑↑s * ξ₀ s t ^ ↑s + ↑↑t * ξ₀ s t ^ ↑t)

theorem Res₀pos (s t : ℕ+) : Res₀ s t > 0

Φ grows exponentially, and we can give explicit coefficients.

theorem ΦAsymptotic (s t : ℕ+) (coprime : s.Coprime t) : Filter.Tendsto (fun (i : ℕ) => ↑(Φ s t ↑i) * (↑(ξ₀ s t) ^ i * ↑(Res₀ s t))) Filter.atTop (nhds 1)

theorem ΦAsymptoticℝ (s t : ℕ+) (coprime : s.Coprime t) : Filter.Tendsto (fun (i : ℕ) => ↑(Φ s t ↑i) * (ξ₀ s t ^ i * Res₀ s t)) Filter.atTop (nhds 1)

theorem ΦAsymptoticℝ' (s t : ℕ+) (coprime : s.Coprime t) : Filter.Tendsto (fun (i : ℤ) => ↑(Φ s t i) * (ξ₀ s t ^ i * Res₀ s t)) Filter.atTop (nhds 1)

As the "inverse function" of Φ, dE grows like log. We first prove it for coprime $s$ and $t$, then generalize it to all integers.

theorem dE_int_Asymptotic_coprime (s t : ℕ+) (coprime : s.Coprime t) : Filter.Tendsto (fun (n : ℝ) => ↑(dE_int s t n) * Real.log (ξ₀ s t) / Real.log n) Filter.atTop (nhds (-1))

theorem reduce_coprime (s t : ℕ+) : ∃ (l : ℕ+) (S : ℕ+) (T : ℕ+), s = l * S ∧ t = l * T ∧ S.Coprime T

theorem dE_int_Asymptotic (s t : ℕ+) : Filter.Tendsto (fun (n : ℝ) => ↑(dE_int s t n) * Real.log (ξ₀ s t) / Real.log n) Filter.atTop (nhds (-1))

wₖ grows linearly w.r.t. nₖ for integer $s$ and $t$. We can then conclude that wₗᵢ, as the linear interpolation, grows at the same rate.

theorem wₖ_Asymtotic (s t : ℕ+) : Filter.Tendsto (fun (k : ℕ) => ↑(wₖ (↑↑s) (↑↑t) k) / ↑(nₖ (↑↑s) (↑↑t) k)) Filter.atTop (nhds (ξ₀ s t ^ ↑t))

theorem lerp_dist (a u v g : ℝ) (arange : a ∈ Set.Icc 0 1) : dist ((1 - a) * u + a * v) g ≤ max (dist u g) (dist v g)

theorem w_Asymtotic_of_wₖ (s t limit : ℝ) [PosReal s] [PosReal t] (wₖas : Filter.Tendsto (fun (k : ℕ) => ↑(wₖ s t k) / ↑(nₖ s t k)) Filter.atTop (nhds limit)) : Filter.Tendsto (fun (n : ℝ) => wₗᵢ s t n / n) Filter.atTop (nhds limit)

theorem w_Asymtotic_int (s t : ℕ+) : Filter.Tendsto (fun (n : ℝ) => wₗᵢ (↑↑s) (↑↑t) n / n) Filter.atTop (nhds (ξ₀ s t ^ ↑t))