Voronovskaja-type Formula for the Bezier Variant of the Bernstein Operators

formal-conjectures · paper · ams-26 · ams-40 · ams-47

The Bézier-type Bernstein operators $B_{n,\alpha}$ for $\alpha > 0$ are defined for
$f : [0,1] \to \mathbb{R}$ by
$$
(B_{n,\alpha} f)(x)
= \sum_{k=0}^n f\!\left(\frac{k}{n}\right)
\left( J_{n,k}(x)^{\alpha} - J_{n,k+1}(x)^{\alpha} \right),
$$
where
$$
J_{n,k}(x) = \sum_{j=k}^n p_{n,j}(x),
\qquad
p_{n,j}(x) = \binom{n}{j} x^j(1-x)^{n-j},
$$
and $J_{n,n+1}(x) = 0$.

In the classical case $\alpha = 1$, these operators reduce to the usual Bernstein operators.
For $f$ which are $C^2$ on $[0,1]$, one has the classical Voronovskaja
asymptotic formula
$$
\lim_{n \to \infty} n\bigl( B_{n,1} f(x) - f(x) \bigr)
= \tfrac{1}{2} x(1-x) f''(x).
$$

Known Results

* For $\alpha = 1$, the asymptotics are completely understood.
* Numerical experiments indicate that for $\alpha \neq 1$ the quantity
$$
\sqrt{n}\,\bigl( B_{n,\alpha} f(x) - f(x) \bigr)
$$
may converge to a non-zero limit.

The Problem

Determine the asymptotic behaviour of the Bézier-type Bernstein operators for $\alpha > 0$,
$\alpha \neq 1$:
\textbf{Existence of the limit:}
Prove (or disprove) the existence of the limit
$$
\lim_{n \to \infty}
\sqrt{n}\,\bigl( B_{n,\alpha} f(x) - f(x) \bigr),
$$
at least for sufficiently smooth functions $f$.
\textbf{Explicit form of the limit:}
If the limit exists, determine an explicit expression for it in terms of $f$, $x$, and $\alpha$.

Existence-only version of the eventual-smoothness variant. This separates the first part of the
source problem, proving that the scaled sequence has some limit, from the stronger task of finding
an explicit expression for that limit.

Mathematical status
Open: marked research open in google-deepmind/formal-conjectures at revision cd3d8db4634733a748b2380f80f77ba3e4b9dda0 (checked 2026-09-11).

Formal availability
A Prop definition is supplied for the pinned Lean 4.33.1 environment and must be accepted by the deployed verifier before it is available.

Sources and provenance
Upstream reference cited by formal-conjectures (checked 2026-09-11): https://www.math.bas.bg/mathmod/Proceedings_CTF/CTF-2010/files_CTF-2010/Open_problems.pdf
Formal statement provenance (Apache-2.0) (checked 2026-09-11): https://github.com/google-deepmind/formal-conjectures/blob/cd3d8db4634733a748b2380f80f77ba3e4b9dda0/FormalConjectures/Paper/VoronovskajaTypeFormula.lean
Local target: Corpus.PaperVoronovskajaTypeFormula.voronovskaja_theorem.bezier_bernstein_operators.variants.eventually_smooth.limit_exists
Source SHA-256: 940145f9b4bc37cc127d7ec43a8c7e9b0f41c72dd0deca2a1d51a748f3cb1274
Lean v4.33.1; Mathlib 0df444a360eaa60ab8c11dca51a86af692955474; policy kernel-replay-v1.
The deployed accepted environment records the actual immutable verifier image.

Research discussions are not verified proofs. A formal target specifies a precise statement; accepting a target does not prove it. Checked results apply to their exact statements and pinned environments.

Public JSON record