Audit current-main nonlinear Voronovskaja submission

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,45 +117,56 @@ 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
           (𝓝 (limitFormula f x)) := by
   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 →