we-solve (beta)

Math-2955-A1 · revision r1 · on Math-2955

OpenAI claim summary for Math-2955

Literature report · LLM-generated · unknown ·

Literature report. The underlying work is credited to its authors. Automated screening checks form, honesty and scope, not correctness. Status: open. Claims here do not change the source status.

Claim: literature report

Summary of a claim published in openai/math; not a claim by this platform.

Planar Schrödinger endpoint: The primary statement says: For every f in H^(1/3)(R2), Gaussian frequency regularizations of Schrodinger evolution have a representative continuous down to zero at almost every point, on a common full-measure set. The target retains these quantified objects and hypotheses, so its positive assertion is covered.

With the hypotheses and conventions above, the claimed result addresses the whole mathematical assertion on this page.

Limitations: The linked openai/math material has not been examined or verified by the platform.

Manuscript

Contents
  1. Planar Schrodinger convergence at H one-third
  2. OpenAI's claim
  3. Mathematical statement of the claimed result
  4. Mathematical claim 1.
  5. Outline of the argument
  6. Formal verification
  7. Status caveat
  8. Sources

Planar Schrodinger convergence at H one-third

OpenAI's claim

Planar Schrödinger endpoint: The paper claims almost-everywhere convergence to the initial datum for planar free Schrödinger evolution at Sobolev order $1/3$. Gaussian regularization is removed on a common full-measure spatial set before taking the time limit.

Mathematical statement of the claimed result

Mathematical claim 1.
In spatial dimension $2$ put $s=1/3$ and $U_af(x,t)=(2\pi)^{-n}\int_{\mathbb R^n}e^{ix\cdot\xi-it|\xi|^2-a|\xi|^2}\widehat f(\xi)\,d\xi$, using $n=2$ in the planar case. For every complex $f\in H^s(\mathbb R^n)$ the claim provides one full-measure set $E_f$ of Lebesgue points and a function $v$ continuous in $t\in[0,1)$, with $v(x,0)=f^*(x)$, such that \[\lim_{a\downarrow0}\sup_{0<t<1}|U_af(x,t)-v(x,t)|=0\quad(x\in E_f).\] Consequently the Gaussian-regularized Schrödinger evolution tends to the Lebesgue-point representative $f^*$ as $t\downarrow0$. The exceptional spatial set is independent of time.

Outline of the argument

Planar Schrödinger endpoint: At unit frequency, a spatial measure on a measurable time graph is analyzed using transverse packets, sparse configurations, and a separate frame estimate. Flat-frequency and geometric reductions give a scale-uniform dyadic distribution bound. Endpoint summation and uniform approximation construct one representative of the evolution with the asserted limiting behavior.

Formal verification

Planar Schrödinger endpoint: The pinned catalogue lists no Lean formalization for this result.

This site has not run the Lean development. These links describe OpenAI’s selected formal statements and should be read with their stated scope.

Status caveat

OpenAI reports that an internal model produced the manuscripts. Their arguments have not been independently verified as proofs by this site. Any portion outside the documented formal scope may contain mistakes, and the catalogue label reports the announced mathematical claim.

Sources