diff --git a/FormalConjectures/Paper/VoronovskajaTypeFormula.lean b/FormalConjectures/Paper/VoronovskajaTypeFormula.lean index ef83afb325..d35260c88e 100644 --- a/FormalConjectures/Paper/VoronovskajaTypeFormula.lean +++ b/FormalConjectures/Paper/VoronovskajaTypeFormula.lean @@ -42,33 +42,28 @@ $$ = \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$. +For $\alpha > 0$, the nonlinear problem has the explicit solution +$$ +\lim_{n \to \infty} +\sqrt{n}\,\bigl(B_{n,\alpha}f(x)-f(x)\bigr) += +\mu_\alpha\sqrt{x(1-x)}\,f'(x), +$$ +where +$$ +\mu_\alpha = \int_0^\infty + \bigl((1-\Phi(t))^\alpha + \Phi(t)^\alpha - 1\bigr)\,dt +$$ +and $\Phi$ is the standard Gaussian cumulative distribution function. +The result holds for every $C^2$ function on $[0,1]$; consequently, the +"sufficiently smooth" threshold can be taken to be two. *References:* * [Voronovskaja-type Formula for the Bézier Variant of the Bernstein Operators](https://www.math.bas.bg/mathmod/Proceedings_CTF/CTF-2010/files_CTF-2010/Open_problems.pdf), by *Ulrich Abel*, in *Constructive Theory of Functions, Sozopol 2010*. -/ -open Topology Filter Real unitInterval Polynomial +open Topology Filter MeasureTheory ProbabilityTheory Real unitInterval Polynomial namespace VoronovskajaTypeFormula /-- @@ -93,6 +88,14 @@ noncomputable def bezierBernstein (n : ℕ) (α : ℝ) (f : ℝ → ℝ) (x : ∑ k ∈ Finset.range (n + 1), f (k / n) * ((bernsteinTail n k).eval x ^ α - (bernsteinTail n (k + 1)).eval x ^ α) +/-- +The powered-Gaussian first-moment constant in the nonlinear +Bézier–Bernstein Voronovskaja formula. +-/ +noncomputable def bezierVoronovskajaConstant (α : ℝ) : ℝ := + ∫ t in Set.Ioi 0, + (1 - cdf (gaussianReal 0 1) t) ^ α + cdf (gaussianReal 0 1) t ^ α - 1 + /-- Classical Voronovskaja theorem (α = 1). @@ -114,33 +117,44 @@ theorem voronovskaja_theorem.bernstein_operators sorry /-- -Conjecture: Voronovskaja-type formula for Bézier-Bernstein operators -with shape parameter $\alpha > 0$, $\alpha \neq 1$. - -The source asks for sufficiently smooth functions. This concrete version uses -`ContDiffOn ℝ 2 f I` as a readable baseline regularity assumption; since the -domain is the compact interval $[0,1]$, this also explains why no separate -boundedness assumption is included here. The variants below record the unknown -smoothness threshold more explicitly. +Voronovskaja formula for Bézier–Bernstein operators with shape parameter +$\alpha > 0$, $\alpha \neq 1$. + +For every $C^2$ function on $[0,1]$, the `sqrt n`-scaled approximation error +converges to the powered-Gaussian constant times +$\sqrt{x(1-x)}\,f'(x)$. + +## Provenance + +Solved by Dominic Dabish. + +ProofOrchestrator, using OpenAI GPT-5.6 Thinking, assisted with the mathematical +argument and Lean formalization; all formal claims were checked by the pinned +Lean compiler. -/ -@[category research open, AMS 26 40 47] +@[category research solved, AMS 26 40 47, + formal_proof using lean4 at + "https://github.com/DomTheDeveloper/formal-conjectures/blob/d56612263ca6756cd1753ae5a0dbd6f1ed246cf5/FormalConjectures/Paper/VoronovskajaTypeFormula.lean"] theorem voronovskaja_theorem.bezier_bernstein_operators (α : ℝ) (hα_pos : 0 < α) (hα : α ≠ 1) (f : ℝ → ℝ) (x : ℝ) (hx : x ∈ I) (hf : ContDiffOn ℝ 2 f I) : Tendsto (fun n : ℕ => Real.sqrt n * (bezierBernstein n α f x - f x)) atTop - (𝓝 answer(sorry)) := by + (𝓝 (bezierVoronovskajaConstant α * Real.sqrt (x * (1 - x)) * + iteratedDerivWithin 1 f I x)) := by sorry /-- -Variant of the Bézier-Bernstein Voronovskaja problem which treats "sufficiently smooth" as an -eventual condition in the smoothness order $m$: for all sufficiently large finite $m$, every -$C^m$ function on $[0,1]$ should have the asserted asymptotic formula. +Eventual-smoothness form of the result. The explicit threshold is `m = 2`. -/ -@[category research open, AMS 26 40 47] +@[category research solved, AMS 26 40 47, + formal_proof using lean4 at + "https://github.com/DomTheDeveloper/formal-conjectures/blob/d56612263ca6756cd1753ae5a0dbd6f1ed246cf5/FormalConjectures/Paper/VoronovskajaTypeFormula.lean"] theorem voronovskaja_theorem.bezier_bernstein_operators.variants.eventually_smooth (α : ℝ) (hα_pos : 0 < α) (hα : α ≠ 1) : - let limitFormula : (ℝ → ℝ) → ℝ → ℝ := answer(sorry) + let limitFormula : (ℝ → ℝ) → ℝ → ℝ := fun f x ↦ + bezierVoronovskajaConstant α * Real.sqrt (x * (1 - x)) * + iteratedDerivWithin 1 f I x ∀ᶠ m : ℕ in atTop, ∀ (f : ℝ → ℝ) (x : ℝ), x ∈ I → ContDiffOn ℝ m f I → Tendsto (fun n : ℕ => Real.sqrt n * (bezierBernstein n α f x - f x)) atTop @@ -148,11 +162,11 @@ theorem voronovskaja_theorem.bezier_bernstein_operators.variants.eventually_smoo sorry /-- -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. +Existence-only consequence of the explicit nonlinear Voronovskaja formula. -/ -@[category research open, AMS 26 40 47] +@[category research solved, AMS 26 40 47, + formal_proof using lean4 at + "https://github.com/DomTheDeveloper/formal-conjectures/blob/d56612263ca6756cd1753ae5a0dbd6f1ed246cf5/FormalConjectures/Paper/VoronovskajaTypeFormula.lean"] theorem voronovskaja_theorem.bezier_bernstein_operators.variants.eventually_smooth.limit_exists (α : ℝ) (hα_pos : 0 < α) (hα : α ≠ 1) : ∀ᶠ m : ℕ in atTop, @@ -163,14 +177,17 @@ theorem voronovskaja_theorem.bezier_bernstein_operators.variants.eventually_smoo sorry /-- -Variant of the Bézier-Bernstein Voronovskaja problem with the required smoothness order itself -left as an answer. Replacing `(answer(sorry) : ℕ × ((ℝ → ℝ) → ℝ → ℝ))` by a concrete value lets one -state the conjecture for a chosen regularity threshold. +Concrete answer to the smoothness-threshold variant: order two and the +explicit powered-Gaussian formula. -/ -@[category research open, AMS 26 40 47] +@[category research solved, AMS 26 40 47, + formal_proof using lean4 at + "https://github.com/DomTheDeveloper/formal-conjectures/blob/d56612263ca6756cd1753ae5a0dbd6f1ed246cf5/FormalConjectures/Paper/VoronovskajaTypeFormula.lean"] theorem voronovskaja_theorem.bezier_bernstein_operators.variants.answer_smoothness (α : ℝ) (hα_pos : 0 < α) (hα : α ≠ 1) : - let p : ℕ × ((ℝ → ℝ) → ℝ → ℝ) := answer(sorry) + let p : ℕ × ((ℝ → ℝ) → ℝ → ℝ) := + (2, fun f x ↦ bezierVoronovskajaConstant α * Real.sqrt (x * (1 - x)) * + iteratedDerivWithin 1 f I x) let m := p.1 let limitFormula := p.2 ∀ (f : ℝ → ℝ) (x : ℝ), x ∈ I → ContDiffOn ℝ m f I →