CounterexampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedprecheck pass

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The Harnack inequality requires nonnegativity

Statement refuted

Statement refuted. There is a positive constant $C$ such that every weak solution $u \in H^{1} (B_{1} (0); R)$ of $- Δ u = 0$ on the unit ball $B_{1} (0) \subset R^{2}$ satisfies $\sup_{B_{1 / 2} (0)} u \leq C \inf_{B_{1 / 2} (0)} u$ .

Counterexample. Take $u (x) = x_{1}$ , the first coordinate. Then $u$ is harmonic, hence a weak solution of $- Δ u = 0$ , but $\sup_{B_{1 / 2} (0)} u = \frac{1}{2}, \inf_{B_{1 / 2} (0)} u = - \frac{1}{2},$ so $\sup \leq C \inf$ fails for every positive constant $C$ : the right-hand side is negative while the left-hand side is $\frac{1}{2}$ . The nonnegativity hypothesis in Harnack inequality for nonnegative weak solutions cannot be omitted; the theorem assumes a nonnegative class on its domain.

Facts & Assumptions

Given: The Axiom of Choice and Countable Choice; the unit ball $B_{1} (0) \subset R^{2}$ ; the linear function $u (x) = x_{1}$ .

[F1]

Harmonic linear functions are weak solutions: $Δ x_{1} = 0$ classically, so $\int_{B_{1}} \nabla u \cdot \nabla v d x = 0$ for every $v \in H_{0}^{1} (B_{1})$ by the divergence theorem, and $u$ is a local weak solution of $- Δ u = 0$ in the sense of Local weak solutions of a divergence-form operator with the coefficients of Uniformly elliptic divergence-form operators and their sesquilinear forms ( $a^{i j} = δ^{i j}$ , $b = c = 0$ ).

[F2]

On the open half-ball $B_{1 / 2} (0)$ , the values $u (x) = x_{1}$ approach $1 / 2$ along $x_{j} = (1 / 2 - 1 / j, 0)$ and $- 1 / 2$ along $y_{j} = (- 1 / 2 + 1 / j, 0)$ for $j > 2$ . Thus $\sup_{B_{1 / 2}} u = 1 / 2$ and $\inf_{B_{1 / 2}} u = - 1 / 2$ , although neither boundary value is attained; by continuity these also equal the essential extrema (The average of a locally integrable function over a Euclidean ball, The essential supremum of a measurable function with respect to a measure).

[F3]

The Harnack statement: for a nonnegative weak solution of $L_{0} u = - F$ one has ${ess sup}_{B_{R / 2}} u \leq C ({ess inf}_{B_{R / 2}} u + R^{2 - n / q} ∥ F ∥_{L^{q} (B_{2 R})})$ ; the sign hypothesis is used in the proof through the test functions with $u^{β}$ for negative exponents and through the weak Harnack inequality (Harnack inequality for nonnegative weak solutions).

Counterexample

1.1givenF1

The linear function is a weak solution. By [F1] $u (x) = x_{1}$ is harmonic on $B_{1} (0)$ and hence a weak solution of $- Δ u = 0$ in the local sense; in particular it belongs to $H^{1} (B_{1} (0))$ and is smooth.

2.1step 1.1F2

The extrema have opposite signs. By [F2], $\sup_{B_{1 / 2} (0)} u = \frac{1}{2}$ and $\inf_{B_{1 / 2} (0)} u = - \frac{1}{2}$ ; therefore for every positive constant $C$ one has $\sup_{B_{1 / 2} (0)} u = \frac{1}{2} > - \frac{1}{2} C = C \inf_{B_{1 / 2} (0)} u$ , so no positive constant satisfies the claimed comparison.

3.1step 2.1F2F3algebra∎

The nonnegativity hypothesis is essential. The function takes both positive and negative values on the half-ball: by [F2], its supremum is $1 / 2$ and its infimum is $- 1 / 2$ . For every positive Harnack constant $C$ , $C \inf_{B_{1 / 2}} u = - C / 2 < 1 / 2 = \sup_{B_{1 / 2}} u$ , so the displayed comparison fails. The theorem uses nonnegativity in the weak-Harnack argument [F3]. All verifications use the explicit linear function, with no choice principle beyond the declared Axiom of Choice and Countable Choice.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

33 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Leon Simon, Lectures on Partial Differential Equations (Stanford University; complete author scan, 118 sheets reproducing the 223 printed pages of the manuscript, two logical pages per sheet) (standard reference, not scraped)
Brian Krummel, Consequences of De Giorgi-Nash-Moser (4 March 2016; complete 7-page notes) (standard reference, not scraped)