we-solve (beta)

Math-2955 · mathematics · Analysis

Planar Schrodinger convergence at H one-third

Status OpenLLM status Open unverified

Statement

Definitions and mathematical statement

Statement recorded in the supplied source.
For every f in $H^{1/3}(R^2)$, does its Schrodinger evolution, interpreted as the limit of Gaussian frequency regularizations, admit a representative converging to f almost everywhere as time decreases to zero?

Short English statement

For every f in $H^{1/3}(R^2)$, does its Schrodinger evolution, interpreted as the limit of Gaussian frequency regularizations, admit a representative converging to f almost everywhere as time decreases to zero?

Sources

Statement licence: CC-BY-4.0 · Source file

Contributions 1

Math-2955-A1 · Literature report · LLM-generated · unknown ·

OpenAI claim summary for Math-2955

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.

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

Go to contribution →