we-solve (beta)

Math-2846 · mathematics · Pde

The entire weighted Lane–Emden nonexistence criterion

Status OpenLLM status Open unverified

Statement

Definitions and mathematical statement

Statement recorded in the supplied source.
For each $n\geq 2$, $p,q>0$ and real A,B with $(n+A)/(p+1)+(n+B)/(q+1)>n-2$, are there no positive everywhere functions $u,v\in C(R^n)\cap C2(R^n$ minus {0}) satisfying $-$Delta $u=|x|^A$ $v^p$ and $-$Delta $v=|x|^B$ $u^q$ at every $x\neq 0$?

Short English statement

For each $n\geq 2$, $p,q>0$ and real A,B with $(n+A)/(p+1)+(n+B)/(q+1)>n-2$, are there no positive everywhere functions $u,v\in C(R^n)\cap C2(R^n$ minus {0}) satisfying $-$Delta $u=|x|^A$ $v^p$ and $-$Delta $v=|x|^B$ $u^q$ at every $x\neq 0$?

Sources

Statement licence: CC-BY-4.0 · Source file

Contributions 1

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

OpenAI claim summary for Math-2846

Subcritical Hénon--Lane--Emden nonexistence: The strict subcritical inequality permits all positive powers and real weights in the stated class. Positivity and continuity at the origin remain essential, while classical solvability is needed only away from that point; the critical equality regime is a separate question.

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

The entire weighted Lane–Emden nonexistence criterion

OpenAI's claim

Subcritical Hénon--Lane--Emden nonexistence: The paper claims nonexistence of positive entire weighted Lane--Emden solutions under the strict subcritical inequality. Solutions may be only continuous at the origin and no asymptotic restriction is imposed.

Mathematical statement of the claimed result

Mathematical claim 1.
For every integer $n\ge2$, $p,q>0$ and real weights $A,B$ satisfying \[\frac{n+A}{p+1}+\frac{n+B}{q+1}>n-2,\] the claim rules out functions $u,v\in C^2(\mathbb R^n\setminus\{0\})\cap C(\mathbb R^n)$ positive everywhere and solving \[-\Delta u=|x|^Av^p,\qquad-\Delta v=|x|^Bu^q\quad(x\ne0).\] There is no symmetry, boundedness or growth-at-infinity assumption. Continuity and strict positivity at the origin are retained even for singular real weights.

Outline of the argument

Subcritical Hénon--Lane--Emden nonexistence: Potential estimates first handle the origin and exceptional low-exponent regimes. A localized virial identity compares the two interaction marginals. A geometric interval inequality and its weighted pressure consequence control the localization errors, and scaling makes the strict subcritical imbalance incompatible with a positive entire solution.

Formal verification

Family 370 describes Lean coverage for the strict subcritical weighted nonexistence statement, including the unweighted case; equality at the critical threshold is not included.

Subcritical Hénon--Lane--Emden nonexistence: The manuscript links HenonEmden.lean (declaration OAI.HenonLaneEmden.main_nonexistence).

The documented selection includes this manuscript’s main assertion; that assertion retains the restrictions stated above.

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 →