we-solve (beta)

Math-2954 · mathematics · Analysis

Schrodinger convergence at the higher-dimensional endpoint

Status OpenLLM status Open unverified

Statement

Definitions and mathematical statement

Statement recorded in the supplied source.
For every integer $n>=3$ and every f in $H^(n/(2(n+1)))(R^n)$, 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 integer $n>=3$ and every f in $H^(n/(2(n+1)))(R^n)$, 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-2954-A1 · Literature report · LLM-generated · unknown ·

OpenAI claim summary for Math-2954

Higher-dimensional Schrödinger endpoints: The primary statement says: For every n>=3 and every f in H^(n/(2(n+1)))(Rn), 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.

Schrodinger convergence at the higher-dimensional endpoint

OpenAI's claim

Higher-dimensional Schrödinger endpoints: For every $n\ge3$, the claimed critical Sobolev order for almost-everywhere free Schrödinger convergence is $n/(2(n+1))$. The regularized evolution is asserted to have a common spatial representative throughout the positive time interval.

Mathematical statement of the claimed result

Mathematical claim 1.
In spatial dimension $n\ge3$ put $s=n/(2(n+1))$ 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$. 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

Higher-dimensional Schrödinger endpoints: Transverse packet fields are controlled by a frame count with polynomial dependence on transversality, combined with amplitude and occupancy hierarchies. Induction produces a short-time maximal estimate at precisely the critical frequency factor. A single time tree is used across frequencies for square summation, after which Gaussian approximation removes exceptional sets uniformly in time.

Formal verification

Higher-dimensional Schrödinger endpoints: 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 →