Kotesovec’s logarithmic limit for A265841

Abstract

The logarithm of the weighted distinct-partition coefficient has Kotesovec’s ratio asymptotic.

Definition 1.1 (The source coefficient).

$$\forall n:\mathbb{N},a\left(n\right)=\mathrm{Polynomial}.\mathrm{coeff}\left((\prod _{k\in \mathrm{Finset}.\mathrm{Icc}\left(1,n\right)}(1+\mathrm{Polynomial}.C\left(k^4\right)\cdot \mathrm{Polynomial}.X^k:\mathrm{Polynomial}\left(\mathbb{N}\right))),n\right)$$

Formalization. D5/S0/Asymptotics/GeneratingFunctions/KotesovecA265841.a (✓ std3).

Citation. OEIS Foundation Inc.; Vaclav Kotesovec (2018). OEIS A022629 and the weighted distinct-partition logarithmic conjectures. URL: https://oeis.org/A022629.

Commentary.

OEIS A265841, NAME (unpaginated): “Expansion of Product_{k>=1} (1 + k^4*x^k).” The coefficient index n ranges over all natural numbers, including zero. Only factors with index at most n contribute to degree n; the empty product gives a(0) = 1.

Definition 1.2 (The source asymptotic).

$$claim=(\mathrm{Filter}.\mathrm{Tendsto}\left((n:\mathbb{N}\mapsto \frac{\mathrm{Real}.\log \left((a\left(n\right):\mathbb{R})\right)}{4\cdot \mathrm{Real}.\mathrm{sqrt}\left(\frac{(n:\mathbb{R})}{2}\right)\cdot \left(\mathrm{Real}.\log \left(2\cdot (n:\mathbb{R})\right)-2\right)}),\mathrm{Filter}.\mathrm{atTop},\mathrm{nhds}\left((1:\mathbb{R})\right)\right))$$

Formalization. D5/S0/Asymptotics/GeneratingFunctions/KotesovecA265841.claim (✓ std3).

Citation. OEIS Foundation Inc.; Vaclav Kotesovec (2018). OEIS A022629 and the weighted distinct-partition logarithmic conjectures. URL: https://oeis.org/A022629.

Commentary.

OEIS A265841, FORMULA (unpaginated): “Conjecture: log(a(n)) ~ 4sqrt(n/2) * (log(2n) - 2).” The symbol ~ means that the real quotient tends to one along all natural indices. Real.log and real division are total at the finitely many indices where their usual positive-domain interpretation does not apply.

Theorem 1.3 (The proved logarithmic limit).

$$\mathrm{Filter}.\mathrm{Tendsto}\left((n:\mathbb{N}\mapsto \frac{\mathrm{Real}.\log \left((a\left(n\right):\mathbb{R})\right)}{4\cdot \mathrm{Real}.\mathrm{sqrt}\left(\frac{(n:\mathbb{R})}{2}\right)\cdot \left(\mathrm{Real}.\log \left(2\cdot (n:\mathbb{R})\right)-2\right)}),\mathrm{Filter}.\mathrm{atTop},\mathrm{nhds}\left((1:\mathbb{R})\right)\right)$$

Proof. Machine-checked in Lean as D5/S0/Asymptotics/GeneratingFunctions/KotesovecA265841.result (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. OEIS Foundation Inc.; Vaclav Kotesovec (2018). OEIS A022629 and the weighted distinct-partition logarithmic conjectures. URL: https://oeis.org/A022629.

Commentary.

A distinct partition whose parts are almost the first M positive integers contributes at least the r-th power of M factorial, where M is the largest index with M(M+1)/2 at most n. Every individual partition has controlled product, and the logarithm of the number of distinct partitions is at most twice the square root of n. The resulting two-sided estimates differ from r times the square root of 2n times (the logarithm of that square root minus one) by at most a constant depending on r times the square root of n. Dividing by the displayed denominator proves the ratio limit. This does not identify an additive second term or a coefficient prefactor.

References

• Truth anchor: D5/S0/Asymptotics/GeneratingFunctions/KotesovecA265841.a
• Truth anchor: D5/S0/Asymptotics/GeneratingFunctions/KotesovecA265841.claim
• Truth anchor: D5/S0/Asymptotics/GeneratingFunctions/KotesovecA265841.result
• Dependency: D5/S0/Asymptotics/GeneratingFunctions/KotesovecA022629