Factorials bounded by powers of the golden ratio

DefinitionGolden factorial exponent#✓fully proved

For a natural number \(n\), the golden factorial exponent \(\alpha(n)\) is the least positive integer \(m\) with \(n! \le \varphi^m\), where \(\varphi\) is the golden ratio. This is the sequence OEIS A214048.

Equivalently \(\alpha(n)\) is the positive integer \(m\) with \(\varphi^{m-1} \le n! \le \varphi^m\); the number \(n!\) is never a power of \(\varphi\) for \(n \ge 2\), and \(\alpha(1) = 1\).

public noncomputable def goldenFactorialExponent (n : ℕ) : ℕ :=
  sInf {m : ℕ | 1 ≤ m ∧ (n.factorial : ℝ) ≤ goldenRatio ^ m}

Sources

• Aleksandar Petojević, Marjana Gorjanac Ranitović, Dragan Rastovac and Milinko Mandić, The Golden Ratio, Factorials, and the Lambert W Function, Journal of Integer Sequences 27 (2024), Article 24.5.7, Section 2.2, definition (4).

Used by 8

Used byMinimality of the golden factorial exponent · Defining property of the golden factorial exponent · Golden factorial exponent of \(1\) · Increment bounds for the golden factorial exponent · Golden factorial exponent of \(2\) · Left factorial bounds at the golden factorial exponent · The golden factorial exponent exceeds the Lambert sequence · Floor formulas for the left factorial

TheoremEvery factorial is at most a positive power of the golden ratio#✓fully proved

Let \(\varphi\) be the golden ratio. For every natural number \(n\) there is an integer \(m \ge 1\) with \(n! \le \varphi^m\).

Thus the set of positive integers \(m\) with \(n! \le \varphi^m\), whose least element is the golden factorial exponent of \(n\), is nonempty.

public theorem exists_goldenRatio_pow_ge_factorial (n : ℕ) :
    ∃ m : ℕ, 1 ≤ m ∧ (n.factorial : ℝ) ≤ goldenRatio ^ m

Sources

• Petojević, Gorjanac Ranitović, Rastovac and Mandić, The Golden Ratio, Factorials, and the Lambert W Function, Journal of Integer Sequences 27 (2024), Article 24.5.7, Section 2.2, definition (4).

Used by 1

Used byDefining property of the golden factorial exponent

TheoremDefining property of the golden factorial exponent#✓fully proved

Let \(\varphi\) be the golden ratio and, for a natural number \(n\), let \(\alpha(n)\) be the least positive integer \(m\) with \(n! \le \varphi^m\). For every natural number \(n\), \(\alpha(n) \ge 1\) and \(n! \le \varphi^{\alpha(n)}\).

public theorem goldenFactorialExponent_mem (n : ℕ) :
    1 ≤ goldenFactorialExponent n ∧
      (n.factorial : ℝ) ≤ goldenRatio ^ goldenFactorialExponent n

Sources

• Petojević, Gorjanac Ranitović, Rastovac and Mandić, The Golden Ratio, Factorials, and the Lambert W Function, Journal of Integer Sequences 27 (2024), Article 24.5.7, Section 2.2, definition (4).

Uses 2 · Used by 2

Statement usesGolden factorial exponent

Proof usesEvery factorial is at most a positive power of the golden ratio

Used byGolden factorial exponent of \(1\) · Golden factorial exponent of \(2\)

TheoremMinimality of the golden factorial exponent#✓fully proved

Let \(\varphi\) be the golden ratio and, for a natural number \(n\), let \(\alpha(n)\) be the least positive integer \(m\) with \(n! \le \varphi^m\). If \(n\) and \(m\) are natural numbers with \(m \ge 1\) and \(n! \le \varphi^m\), then \(\alpha(n) \le m\).

public theorem goldenFactorialExponent_le {n m : ℕ} (hm : 1 ≤ m)
    (h : (n.factorial : ℝ) ≤ goldenRatio ^ m) : goldenFactorialExponent n ≤ m

Sources

• Petojević, Gorjanac Ranitović, Rastovac and Mandić, The Golden Ratio, Factorials, and the Lambert W Function, Journal of Integer Sequences 27 (2024), Article 24.5.7, Section 2.2, definition (4).

Uses 1 · Used by 2

Statement usesGolden factorial exponent

Used byGolden factorial exponent of \(1\) · Golden factorial exponent of \(2\)

TheoremGolden factorial exponent of \(1\)#✓fully proved

Let \(\varphi\) be the golden ratio and, for a natural number \(n\), let \(\alpha(n)\) be the least positive integer \(m\) with \(n! \le \varphi^m\). Then \(\alpha(1) = 1\).

public theorem goldenFactorialExponent_one : goldenFactorialExponent 1 = 1

Sources

• Petojević, Gorjanac Ranitović, Rastovac and Mandić, The Golden Ratio, Factorials, and the Lambert W Function, Journal of Integer Sequences 27 (2024), Article 24.5.7, Table 3.

Uses 3

Statement usesGolden factorial exponent

Proof usesMinimality of the golden factorial exponent · Defining property of the golden factorial exponent

TheoremGolden factorial exponent of \(2\)#✓fully proved

Let \(\varphi\) be the golden ratio and, for a natural number \(n\), let \(\alpha(n)\) be the least positive integer \(m\) with \(n! \le \varphi^m\). Then \(\alpha(2) = 2\).

This holds because \(\varphi < 2 \le \varphi^2 = \varphi + 1\).

public theorem goldenFactorialExponent_two : goldenFactorialExponent 2 = 2

Sources

• Petojević, Gorjanac Ranitović, Rastovac and Mandić, The Golden Ratio, Factorials, and the Lambert W Function, Journal of Integer Sequences 27 (2024), Article 24.5.7, Table 3.

Uses 3

Statement usesGolden factorial exponent

Proof usesMinimality of the golden factorial exponent · Defining property of the golden factorial exponent

DefinitionAlternating-sign Fibonacci sequence#✓fully proved

The alternating-sign Fibonacci sequence (OEIS A181716) is the integer sequence \((d_m)_{m \ge 0}\) defined by \(d_0 = 0\), \(d_1 = 1\) and \(d_{m+2} = d_{m+1} + d_m + (-1)^{m+2}\) for every natural number \(m\).

public def alternatingSignFibonacci : ℕ → ℤ
  | 0 => 0
  | 1 => 1
  | m + 2 => alternatingSignFibonacci (m + 1) + alternatingSignFibonacci m + (-1) ^ (m + 2)

Sources

• Petojević, Gorjanac Ranitović, Rastovac and Mandić, The Golden Ratio, Factorials, and the Lambert W Function, Journal of Integer Sequences 27 (2024), Article 24.5.7, Section 2.2 (definition before Lemma 3).

Used by 3

Used byRecurrence of the alternating-sign Fibonacci sequence · First values of the alternating-sign Fibonacci sequence · Counting integers by their golden-ratio logarithm

TheoremRecurrence of the alternating-sign Fibonacci sequence#✓fully proved

For every natural number \(m\), the alternating-sign Fibonacci sequence \(d\) satisfies \(d_{m+2} = d_{m+1} + d_m + (-1)^{m+2}\).

public theorem alternatingSignFibonacci_add_two (m : ℕ) :
    alternatingSignFibonacci (m + 2) =
      alternatingSignFibonacci (m + 1) + alternatingSignFibonacci m + (-1) ^ (m + 2)

Sources

• Petojević, Gorjanac Ranitović, Rastovac and Mandić, The Golden Ratio, Factorials, and the Lambert W Function, Journal of Integer Sequences 27 (2024), Article 24.5.7, Section 2.2.

Uses 1

Statement usesAlternating-sign Fibonacci sequence

TheoremFirst values of the alternating-sign Fibonacci sequence#✓fully proved

The alternating-sign Fibonacci sequence \(d\) satisfies \(d_0 = 0\), \(d_1 = 1\), \(d_2 = 2\), \(d_3 = 2\) and \(d_4 = 5\).

public theorem alternatingSignFibonacci_small_values :
    alternatingSignFibonacci 0 = 0 ∧ alternatingSignFibonacci 1 = 1 ∧
      alternatingSignFibonacci 2 = 2 ∧ alternatingSignFibonacci 3 = 2 ∧
      alternatingSignFibonacci 4 = 5

Sources

• Petojević, Gorjanac Ranitović, Rastovac and Mandić, The Golden Ratio, Factorials, and the Lambert W Function, Journal of Integer Sequences 27 (2024), Article 24.5.7, Example 5.

Uses 1

Statement usesAlternating-sign Fibonacci sequence

DefinitionKurepa's partial integral#✓fully proved

For a natural number \(n\) and a real number \(x\), Kurepa's partial integral is

\[K_n(x) = \int_0^x e^{-t} \sum_{k=0}^{n-1} t^k \, dt,\]

an oriented integral, so for \(x < 0\) it is minus the integral over \([x, 0]\).

The paper writes it as \(!n(x) = \int_0^x e^{-t} \frac{t^n - 1}{t - 1} \, dt\); the geometric sum agrees with \(\frac{t^n - 1}{t - 1}\) for \(t \ne 1\), and the singularity at \(t = 1\) is removable.

public noncomputable def kurepaPartialIntegral (n : ℕ) (x : ℝ) : ℝ :=
  ∫ t in (0 : ℝ)..x, Real.exp (-t) * ∑ k ∈ Finset.range n, t ^ k

Sources

• Petojević, Gorjanac Ranitović, Rastovac and Mandić, The Golden Ratio, Factorials, and the Lambert W Function, Journal of Integer Sequences 27 (2024), Article 24.5.7, Section 1 (the function !z(x)) and Sections 3.1-3.3.

Used by 5

Used byLeft factorial bounds at the golden factorial exponent · Lambert bounds for the left factorial · Two-parameter Lambert bounds for the left factorial · Kurepa's partial integral vanishes at zero · Floor formulas for the left factorial

TheoremKurepa's partial integral vanishes at zero#✓fully proved

For every natural number \(n\), Kurepa's partial integral \(K_n(x) = \int_0^x e^{-t} \sum_{k=0}^{n-1} t^k \, dt\) satisfies \(K_n(0) = 0\).

public theorem kurepaPartialIntegral_zero (n : ℕ) : kurepaPartialIntegral n 0 = 0

Sources

• Petojević, Gorjanac Ranitović, Rastovac and Mandić, The Golden Ratio, Factorials, and the Lambert W Function, Journal of Integer Sequences 27 (2024), Article 24.5.7, Section 1.

Uses 1

Statement usesKurepa's partial integral

TheoremIncrement bounds for the golden factorial exponent#●ready to prove

Let \(\varphi\) be the golden ratio and, for a natural number \(n\), let \(\alpha(n)\) be the least positive integer \(m\) with \(n! \le \varphi^m\). For every natural number \(n > 1\),

\[\alpha(n-1) + \lfloor \log_\varphi n \rfloor \le \alpha(n) \le \alpha(n-1) + \lfloor \log_\varphi n \rfloor + 1.\]

public theorem_wanted goldenFactorialExponent_succ_bounds (n : ℕ) (hn : 1 < n) :
    goldenFactorialExponent (n - 1) + ⌊Real.logb goldenRatio n⌋₊ ≤
        goldenFactorialExponent n ∧
      goldenFactorialExponent n ≤
        goldenFactorialExponent (n - 1) + ⌊Real.logb goldenRatio n⌋₊ + 1

Sources

• Petojević, Gorjanac Ranitović, Rastovac and Mandić, The Golden Ratio, Factorials, and the Lambert W Function, Journal of Integer Sequences 27 (2024), Article 24.5.7, Lemma 2 (jis-2024-24.5.7-lem-2).

Uses 1

Statement usesGolden factorial exponent

TheoremCounting integers by their golden-ratio logarithm#●ready to prove

Let \(d\) be the integer sequence with \(d(0) = 0\), \(d(1) = 1\) and \(d(m) = d(m-1) + d(m-2) + (-1)^m\) for \(m \ge 2\), and let \(\varphi\) be the golden ratio. For every integer \(m \ge 1\), the number of positive integers \(n\) with \(\lfloor \log_\varphi n \rfloor = m\) equals \(d(m)\).

public theorem_wanted ncard_floor_logb_goldenRatio_eq_alternatingSignFibonacci (m : ℕ)
    (hm : 1 ≤ m) :
    (({n : ℕ | 1 ≤ n ∧ ⌊Real.logb goldenRatio n⌋₊ = m}.ncard : ℕ) : ℤ) =
      alternatingSignFibonacci m

Sources

• Petojević, Gorjanac Ranitović, Rastovac and Mandić, The Golden Ratio, Factorials, and the Lambert W Function, Journal of Integer Sequences 27 (2024), Article 24.5.7, Lemma 3 (jis-2024-24.5.7-lem-3).

Uses 1

Statement usesAlternating-sign Fibonacci sequence

TheoremExistence of the Lambert sequences#✓fully proved

Let \(h(y) = y e^y\) be the Lambert map. For every natural number \(n \ge 4\) and every real number \(c\) with \(0 < c \le 1\) there is a real number \(a \ge n - 1\) with

\[h\left(-\frac{a}{n-1}\right) = -\frac{1}{n-1} \, c^{1/(n-1)}.\]

Equivalently, \(a = -(n-1) \, W_{-1}\left(-\frac{1}{n-1} c^{1/(n-1)}\right)\), where \(W_{-1}\) is the lower real branch of the Lambert W function. With \(c = 4/7\) this is the paper's \(a_n\), and with \(c = 4/(7m)\) for an integer \(m \ge 1\) it is the paper's \(A_{n,m}\).

public theorem exists_lambertSequence {n : ℕ} (hn : 4 ≤ n) {c : ℝ} (hc0 : 0 < c)
    (hc1 : c ≤ 1) :
    ∃ a : ℝ, (n : ℝ) - 1 ≤ a ∧
      lambertMap (-a / ((n : ℝ) - 1)) = -(1 / ((n : ℝ) - 1)) * c ^ (1 / ((n : ℝ) - 1))

Sources

• Petojević, Gorjanac Ranitović, Rastovac and Mandić, The Golden Ratio, Factorials, and the Lambert W Function, Journal of Integer Sequences 27 (2024), Article 24.5.7, Section 3.1 (the lower branch W₋₁ defining a n and A n m).

Uses 2

Statement usesLambert map

Proof usesLower-branch preimages of the Lambert map

TheoremThe golden factorial exponent exceeds the Lambert sequence#●ready to prove

Let \(n > 4\) be an integer, let \(h(y) = y e^y\) be the Lambert map, and let \(a\) be a real number with \(a \ge n - 1\) and

\[h\left(-\frac{a}{n-1}\right) = -\frac{1}{n-1}\left(\frac{4}{7}\right)^{1/(n-1)}.\]

Then \(a < \alpha(n)\), where \(\alpha(n)\) is the least positive integer \(m\) with \(n! \le \varphi^m\) and \(\varphi\) is the golden ratio.

The two conditions on \(a\) say exactly that \(a = -(n-1)\, W_{-1}\left(-\frac{1}{n-1}\left(\frac{4}{7}\right)^{1/(n-1)}\right)\), where \(W_{-1}\) is the lower real branch of the Lambert \(W\) function; this is the paper's \(a(n)\).

public theorem_wanted lambertSequence_lt_goldenFactorialExponent (n : ℕ) (hn : 4 < n)
    (a : ℝ) (ha : (n : ℝ) - 1 ≤ a)
    (hW : lambertMap (-a / ((n : ℝ) - 1)) =
      -(1 / ((n : ℝ) - 1)) * (4 / 7 : ℝ) ^ (1 / ((n : ℝ) - 1))) :
    a < goldenFactorialExponent n

Sources

• Petojević, Gorjanac Ranitović, Rastovac and Mandić, The Golden Ratio, Factorials, and the Lambert W Function, Journal of Integer Sequences 27 (2024), Article 24.5.7, Theorem 6 (jis-2024-24.5.7-thm-6).

Uses 2

Statement usesGolden factorial exponent · Lambert map

TheoremA linear lower bound for the Lambert sequence#●ready to prove

Let \(n \ge 4\) be a natural number, write \(h(y) = y e^y\) for the Lambert map, and let \(a\) be a real number with \(a \ge n - 1\) such that

\[h\left(-\frac{a}{n - 1}\right) = -\frac{1}{n - 1} \left(\frac{4}{7}\right)^{1/(n - 1)}.\]

Then \(2n - 4 < \frac{3}{4} a\).

These conditions determine \(a\) uniquely: it is the paper's \(a_n = -(n - 1) W_{-1}\bigl(-\frac{1}{n - 1} (4/7)^{1/(n - 1)}\bigr)\), where \(W_{-1}\) is the lower real branch of the Lambert W function.

public theorem_wanted two_mul_sub_four_lt_lambertSequence (n : ℕ) (hn : 4 ≤ n)
    (a : ℝ) (ha : (n : ℝ) - 1 ≤ a)
    (hW : lambertMap (-a / ((n : ℝ) - 1)) =
      -(1 / ((n : ℝ) - 1)) * (4 / 7 : ℝ) ^ (1 / ((n : ℝ) - 1))) :
    2 * (n : ℝ) - 4 < 3 / 4 * a

Sources

• Petojević, Gorjanac Ranitović, Rastovac and Mandić, The Golden Ratio, Factorials, and the Lambert W Function, Journal of Integer Sequences 27 (2024), Article 24.5.7, Lemma 8 (jis-2024-24.5.7-lem-8).

Uses 1

Statement usesLambert map

TheoremPartial exponential sums at the Lambert sequence#●ready to prove

Let \(n \ge 5\) and \(k\) be natural numbers with \(k < n - 2\), let \(h(y) = y e^y\) be the Lambert map, and let \(a\) be a real number with \(a \ge n - 1\) and

\[h\left(-\frac{a}{n-1}\right) = -\frac{1}{n-1}\left(\frac{4}{7}\right)^{1/(n-1)}.\]

Then

\[\sum_{t=0}^{k} \frac{a^t}{t!} < \frac{a^{k+1}}{(k+1)!}.\]

The two conditions on \(a\) say exactly that \(a = -(n-1)\, W_{-1}\left(-\frac{1}{n-1}\left(\frac{4}{7}\right)^{1/(n-1)}\right)\), where \(W_{-1}\) is the lower real branch of the Lambert \(W\) function; this is the paper's \(a(n)\).

public theorem_wanted sum_pow_div_factorial_lt_lambertSequence (n k : ℕ) (hn : 5 ≤ n)
    (hk : k < n - 2) (a : ℝ) (ha : (n : ℝ) - 1 ≤ a)
    (hW : lambertMap (-a / ((n : ℝ) - 1)) =
      -(1 / ((n : ℝ) - 1)) * (4 / 7 : ℝ) ^ (1 / ((n : ℝ) - 1))) :
    ∑ t ∈ Finset.range (k + 1), a ^ t / (t.factorial : ℝ) <
      a ^ (k + 1) / ((k + 1).factorial : ℝ)

Sources

• Petojević, Gorjanac Ranitović, Rastovac and Mandić, The Golden Ratio, Factorials, and the Lambert W Function, Journal of Integer Sequences 27 (2024), Article 24.5.7, Lemma 9 (jis-2024-24.5.7-lem-9).

Uses 1

Statement usesLambert map

TheoremLambert bounds for the left factorial#●ready to prove

Let \(n \ge 5\) be an integer, let \(!n = \sum_{k=0}^{n-1} k!\) be the left factorial, let \(K_n(x) = \int_0^x e^{-t} \sum_{k=0}^{n-1} t^k \, dt\) be Kurepa's partial integral, let \(h(y) = y e^y\) be the Lambert map, and let \(a\) be a real number with \(a \ge n - 1\) and

\[h\left(-\frac{a}{n-1}\right) = -\frac{1}{n-1}\left(\frac{4}{7}\right)^{1/(n-1)}.\]

Then \(K_n(a) < {!n} < K_n(a) + 1\).

The two conditions on \(a\) say exactly that \(a = -(n-1)\, W_{-1}\left(-\frac{1}{n-1}\left(\frac{4}{7}\right)^{1/(n-1)}\right)\), where \(W_{-1}\) is the lower real branch of the Lambert \(W\) function; this is the paper's \(a(n)\), and \(K_n(a)\) is its \(b(n)\).

public theorem_wanted kurepaPartialIntegral_lambertSequence_bounds (n : ℕ) (hn : 5 ≤ n)
    (a : ℝ) (ha : (n : ℝ) - 1 ≤ a)
    (hW : lambertMap (-a / ((n : ℝ) - 1)) =
      -(1 / ((n : ℝ) - 1)) * (4 / 7 : ℝ) ^ (1 / ((n : ℝ) - 1))) :
    kurepaPartialIntegral n a < ∑ k ∈ Finset.range n, (k.factorial : ℝ) ∧
      ∑ k ∈ Finset.range n, (k.factorial : ℝ) < kurepaPartialIntegral n a + 1

Sources

• Petojević, Gorjanac Ranitović, Rastovac and Mandić, The Golden Ratio, Factorials, and the Lambert W Function, Journal of Integer Sequences 27 (2024), Article 24.5.7, Theorem 10 (jis-2024-24.5.7-thm-10).

Uses 2

Statement usesKurepa's partial integral · Lambert map

TheoremLeft factorial bounds at the golden factorial exponent#●ready to prove

For every integer \(n \ge 1\), let \(!n = \sum_{k=0}^{n-1} k!\) be the left factorial, let \(K_n(x) = \int_0^x e^{-t} \sum_{k=0}^{n-1} t^k \, dt\) be Kurepa's partial integral, and let \(\alpha(n)\) be the least positive integer \(m\) with \(n! \le \varphi^m\), where \(\varphi\) is the golden ratio. Then \(\beta(n) = K_n(\alpha(n))\) satisfies \(\beta(n) < {!n} < \beta(n) + 1\).

public theorem_wanted kurepaPartialIntegral_goldenFactorialExponent_bounds (n : ℕ)
    (hn : 1 ≤ n) :
    kurepaPartialIntegral n (goldenFactorialExponent n) <
        ∑ k ∈ Finset.range n, (k.factorial : ℝ) ∧
      ∑ k ∈ Finset.range n, (k.factorial : ℝ) <
        kurepaPartialIntegral n (goldenFactorialExponent n) + 1

Sources

• Petojević, Gorjanac Ranitović, Rastovac and Mandić, The Golden Ratio, Factorials, and the Lambert W Function, Journal of Integer Sequences 27 (2024), Article 24.5.7, Theorem 12 (jis-2024-24.5.7-thm-12).

Uses 2

Statement usesGolden factorial exponent · Kurepa's partial integral

TheoremTwo-parameter Lambert bounds for the left factorial#●ready to prove

Let \(n \ge 5\) and \(m \ge 1\) be integers, let \(!n = \sum_{k=0}^{n-1} k!\) be the left factorial, let \(K_n(x) = \int_0^x e^{-t} \sum_{k=0}^{n-1} t^k \, dt\) be Kurepa's partial integral, let \(h(y) = y e^y\) be the Lambert map, and let \(A\) be a real number with \(A \ge n - 1\) and

\[h\left(-\frac{A}{n-1}\right) = -\frac{1}{n-1}\left(\frac{4}{7m}\right)^{1/(n-1)}.\]

Then \(K_n(A) < {!n} < K_n(A) + \frac{1}{m}\).

The two conditions on \(A\) say exactly that \(A = -(n-1)\, W_{-1}\left(-\frac{1}{n-1}\left(\frac{4}{7m}\right)^{1/(n-1)}\right)\), where \(W_{-1}\) is the lower real branch of the Lambert \(W\) function; this is the paper's \(A(n, m)\), and \(K_n(A)\) is its \(B(n, m)\).

public theorem_wanted kurepaPartialIntegral_lambertSequence_two_bounds (n m : ℕ)
    (hn : 5 ≤ n) (hm : 1 ≤ m) (A : ℝ) (hA : (n : ℝ) - 1 ≤ A)
    (hW : lambertMap (-A / ((n : ℝ) - 1)) =
      -(1 / ((n : ℝ) - 1)) * (4 / (7 * m) : ℝ) ^ (1 / ((n : ℝ) - 1))) :
    kurepaPartialIntegral n A < ∑ k ∈ Finset.range n, (k.factorial : ℝ) ∧
      ∑ k ∈ Finset.range n, (k.factorial : ℝ) < kurepaPartialIntegral n A + 1 / m

Sources

• Petojević, Gorjanac Ranitović, Rastovac and Mandić, The Golden Ratio, Factorials, and the Lambert W Function, Journal of Integer Sequences 27 (2024), Article 24.5.7, Theorem 14 (jis-2024-24.5.7-thm-14).

Uses 2

Statement usesKurepa's partial integral · Lambert map

TheoremFloor formulas for the left factorial#●ready to prove

Let \(!n = \sum_{k=0}^{n-1} k!\) be the left factorial, let \(K_n(x) = \int_0^x e^{-t} \sum_{k=0}^{n-1} t^k \, dt\) be Kurepa's partial integral, let \(h(y) = y e^y\) be the Lambert map, and let \(\alpha(n)\) be the least positive integer \(m\) with \(n! \le \varphi^m\), where \(\varphi\) is the golden ratio. Then the following hold. (i) For every integer \(n \ge 1\), \(\lfloor K_n(\alpha(n)) \rfloor + 1 = {!n}\). (ii) For every integer \(n > 4\) and every real \(a \ge n - 1\) with \(h(-\frac{a}{n-1}) = -\frac{1}{n-1} (\frac{4}{7})^{1/(n-1)}\), we have \(\lfloor K_n(a) \rfloor + 1 = {!n}\). (iii) For all integers \(n > 4\) and \(m \ge 1\) and every real \(A \ge n - 1\) with \(h(-\frac{A}{n-1}) = -\frac{1}{n-1} (\frac{4}{7m})^{1/(n-1)}\), we have \(\lfloor K_n(A) + \frac{1}{m} \rfloor = {!n}\).

public theorem_wanted leftFactorial_eq_floor_kurepaPartialIntegral :
    (∀ n : ℕ, 1 ≤ n →
      ⌊kurepaPartialIntegral n (goldenFactorialExponent n)⌋ + 1 =
        ∑ k ∈ Finset.range n, (k.factorial : ℤ)) ∧
    (∀ n : ℕ, 4 < n → ∀ a : ℝ, (n : ℝ) - 1 ≤ a →
      lambertMap (-a / ((n : ℝ) - 1)) =
        -(1 / ((n : ℝ) - 1)) * (4 / 7 : ℝ) ^ (1 / ((n : ℝ) - 1)) →
      ⌊kurepaPartialIntegral n a⌋ + 1 = ∑ k ∈ Finset.range n, (k.factorial : ℤ)) ∧
    (∀ n m : ℕ, 4 < n → 1 ≤ m → ∀ A : ℝ, (n : ℝ) - 1 ≤ A →
      lambertMap (-A / ((n : ℝ) - 1)) =
        -(1 / ((n : ℝ) - 1)) * (4 / (7 * m) : ℝ) ^ (1 / ((n : ℝ) - 1)) →
      ⌊kurepaPartialIntegral n A + 1 / m⌋ = ∑ k ∈ Finset.range n, (k.factorial : ℤ))

Sources

• Petojević, Gorjanac Ranitović, Rastovac and Mandić, The Golden Ratio, Factorials, and the Lambert W Function, Journal of Integer Sequences 27 (2024), Article 24.5.7, Corollary 15 (jis-2024-24.5.7-cor-15).

Uses 3

Statement usesGolden factorial exponent · Kurepa's partial integral · Lambert map

12 fully proved9 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.