LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)

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 envelopes are the least upper and greatest lower semicontinuous functions

Statement

Let $A \subseteq R^{m}$ be nonempty and let $u : A \to R$ be bounded, with envelopes $u^{*}, u_{*}$ as in Upper and lower semicontinuous envelopes by local limsup and liminf. Then $u^{*}$ is upper semicontinuous on $A$ , $u_{*}$ is lower semicontinuous on $A$ , and $u_{*} \leq u \leq u^{*}$ pointwise. Moreover: (1) $u^{*}$ is the least upper semicontinuous function $w : A \to \overline{R}$ with $w \geq u$ pointwise, and $u^{*} = u$ if and only if $u$ is upper semicontinuous; (2) $u_{*}$ is the greatest lower semicontinuous function $w : A \to \overline{R}$ with $w \leq u$ pointwise, and $u_{*} = u$ if and only if $u$ is lower semicontinuous; (3) $(u^{*})^{*} = u^{*}$ and $(u_{*})_{*} = u_{*}$ . No choice principle is used.

Facts & Assumptions

Given: A nonempty set $A \subseteq R^{m}$ , a bounded function $u : A \to R$ , the local suprema $M_{r} (x) = \sup {u (y) : y \in A, ∣ y - x ∣ \leq r}$ and local infima $m_{r} (x) = \inf {u (y) : y \in A, ∣ y - x ∣ \leq r}$ for $x \in A$ , $r > 0$ , all computed in $\overline{R}$ , and the envelopes $u^{*} (x) = \inf_{r > 0} M_{r} (x)$ , $u_{*} (x) = \sup_{r > 0} m_{r} (x)$ .

[F1]

For every $x \in A$ the sets ${M_{r} (x) : r > 0}$ and ${m_{r} (x) : r > 0}$ are nonempty and bounded (by the bounds of $u$ ); $u^{*} (x) = \inf_{r > 0} M_{r} (x)$ is the greatest lower bound of the first set, $u_{*} (x) = \sup_{r > 0} m_{r} (x)$ is the least upper bound of the second, and $m_{r} (x) \leq u (x) \leq M_{r} (x)$ for every $r > 0$ . In particular $u^{*} (x) \leq M_{r} (x)$ and $m_{r} (x) \leq u_{*} (x)$ for every $r > 0$ (Upper and lower semicontinuous envelopes by local limsup and liminf).

[F2]

For real-valued functions, upper and lower semicontinuity have the local $ε$ characterizations: near $a$ , respectively $f (x) < f (a) + ε$ and $f (x) > f (a) - ε$ (Upper and lower semicontinuity on subsets of $R^{n}$ ). For an extended-real upper semicontinuous $w$ , we use the standard strict-sublevel convention ${w < c}$ open for every real $c$ ; if $w (a)$ is finite, applying it with $c = w (a) + ε$ gives the same local upper bound. The dual strict-superlevel convention for lower semicontinuity gives the local lower bound when $w (a)$ is finite. These are exactly the finite-value cases used in steps 1.3 and 1.4; the infinite endpoint cases are disposed of there directly.

[F3]

If $S \subseteq R$ is nonempty and $ℓ = \inf S$ , then $ℓ \leq s$ for every $s \in S$ , and $ℓ^{'} \leq ℓ$ for every lower bound $ℓ^{'}$ of $S$ (Greatest lower bound (infimum)).

[F4]

If $S \subseteq R$ is nonempty, bounded above and $v \in R$ is an upper bound of $S$ , then $v = \sup S$ if and only if for every $ε > 0$ there is $s \in S$ with $v - ε < s$ ; in particular a supremum of $S$ in $R$ is an upper bound of $S$ (Epsilon characterisation of the supremum).

Proof

technique · monotone localisation; the envelopes are compared with a competing semicontinuous function by testing the defining infimum and supremum

1.1F1F2F3F4algebra

$u^{*}$ is upper semicontinuous on $A$ and $u_{*} \leq u \leq u^{*}$ . Fix $x \in A$ and $ε > 0$ . Since $u^{*} (x) + 2^{- 1} ε > u^{*} (x)$ is not a lower bound of the nonempty set ${M_{r} (x) : r > 0}$ by the leastness clause of [F3], there is $r > 0$ with $M_{r} (x) < u^{*} (x) + 2^{- 1} ε$ . For $z \in A$ with $∣ z - x ∣ < r$ put $δ : = r - ∣ z - x ∣ > 0$ ; every $w \in A$ with $∣ w - z ∣ \leq δ$ satisfies $∣ w - x ∣ \leq ∣ w - z ∣ + ∣ z - x ∣ \leq r$ , so the set defining $M_{δ} (z)$ is contained in the set defining $M_{r} (x)$ and therefore $M_{δ} (z) \leq M_{r} (x) < u^{*} (x) + 2^{- 1} ε$ ; since $u^{*} (z) \leq M_{δ} (z)$ by [F1], we get $u^{*} (z) < u^{*} (x) + ε$ . Thus $u^{*}$ is upper semicontinuous at $x$ by [F2], and $x$ was arbitrary. Next, $u (x)$ is a lower bound of ${M_{r} (x) : r > 0}$ by [F1], so $u (x) \leq u^{*} (x)$ by the greatest-lower-bound clause of [F3]. Finally $u (x)$ is an upper bound of ${m_{r} (x) : r > 0}$ by [F1]; if $u_{*} (x) > u (x)$ held, then $η : = u_{*} (x) - u (x) > 0$ and [F4] would give $r > 0$ with $u_{*} (x) - η < m_{r} (x)$ , that is $u (x) < m_{r} (x)$ , contradicting $m_{r} (x) \leq u (x)$ ; hence $u_{*} (x) \leq u (x)$ .

1.2F1F2F4algebra

$u_{*}$ is lower semicontinuous on $A$ . Fix $x \in A$ and $ε > 0$ . By [F4] applied to the nonempty bounded-above set ${m_{r} (x) : r > 0}$ with supremum $u_{*} (x)$ , there is $r > 0$ with $u_{*} (x) - ε < m_{r} (x)$ . For $z \in A$ with $∣ z - x ∣ < r$ put $δ : = r - ∣ z - x ∣ > 0$ ; every $w \in A$ with $∣ w - z ∣ \leq δ$ satisfies $∣ w - x ∣ \leq r$ , so $m_{δ} (z) \geq m_{r} (x)$ , and $u_{*} (z) \geq m_{δ} (z)$ by [F1]; hence $u_{*} (z) > u_{*} (x) - ε$ , which is lower semicontinuity at $x$ by [F2].

1.3F1F2F3algebra

Least upper semicontinuous majorant. Let $w : A \to \overline{R}$ be upper semicontinuous with $w \geq u$ , fix $x \in A$ and $ε > 0$ . Since $w \geq u$ and $u$ is real-valued, $w$ takes no value $- \infty$ ; if $w (x) = + \infty$ then $u^{*} (x) \leq w (x)$ holds because $u^{*}$ is real-valued by [F1] and boundedness of $u$ , so assume $w (x) \in R$ . By [F2] there is $r_{0} > 0$ with $w (y) < w (x) + ε$ for all $y \in A$ with $∣ y - x ∣ < r_{0}$ . For $y \in A$ with $∣ y - x ∣ \leq r_{0} / 2$ we then have $u (y) \leq w (y) < w (x) + ε$ , so $w (x) + ε$ is an upper bound of the set defining $M_{r_{0} / 2} (x)$ , whence $M_{r_{0} / 2} (x) \leq w (x) + ε$ . Since $u^{*} (x) = \inf_{r > 0} M_{r} (x) \leq M_{r_{0} / 2} (x)$ by [F3], we get $u^{*} (x) \leq w (x) + ε$ , and letting $ε ↓ 0$ gives $u^{*} (x) \leq w (x)$ . Hence $u^{*} \leq w$ for every upper semicontinuous majorant $w$ of $u$ .

1.4F1F2algebra

Greatest lower semicontinuous minorant. Let $w : A \to \overline{R}$ be lower semicontinuous with $w \leq u$ , fix $x \in A$ and $ε > 0$ . Since $w \leq u$ , $w (x) \in R \cup {- \infty}$ ; if $w (x) = - \infty$ then $u_{*} (x) \geq w (x)$ is automatic, so assume $w (x) \in R$ . By [F2] there is $r_{0} > 0$ with $w (y) > w (x) - ε$ for all $y \in A$ with $∣ y - x ∣ < r_{0}$ . For $y \in A$ with $∣ y - x ∣ \leq r_{0} / 2$ we have $w (y) > w (x) - ε$ and $w (y) \leq u (y)$ , so $w (x) - ε$ is a lower bound of the set defining $m_{r_{0} / 2} (x)$ , whence $m_{r_{0} / 2} (x) \geq w (x) - ε$ . Since $u_{*} (x)$ is an upper bound of ${m_{r} (x) : r > 0}$ by [F1], we get $u_{*} (x) \geq m_{r_{0} / 2} (x) \geq w (x) - ε$ , and letting $ε ↓ 0$ gives $u_{*} (x) \geq w (x)$ .

2.1step 1.1step 1.2step 1.3step 1.4

The two equivalences. If $u$ is upper semicontinuous, then $u$ is an upper semicontinuous majorant of itself, so $u^{*} \leq u$ by step 1.3; with $u \leq u^{*}$ from step 1.1 this gives $u^{*} = u$ . Conversely, if $u^{*} = u$ , then $u$ is upper semicontinuous because $u^{*}$ is, by step 1.1. The same two lines with step 1.4 and step 1.2 show that $u_{*} = u$ if and only if $u$ is lower semicontinuous.

3.1step 1.1step 1.2step 2.1∎

Idempotence. The function $u^{*}$ is bounded and upper semicontinuous on $A$ by step 1.1, and it is its own upper semicontinuous majorant; applying the equivalence of step 2.1 to $u^{*}$ in place of $u$ gives $(u^{*})^{*} = u^{*}$ . Likewise $u_{*}$ is bounded and lower semicontinuous by steps 1.1 and 1.2, so $(u_{*})_{*} = u_{*}$ .

Remarks

Where boundedness is used. Boundedness of $u$ keeps every $M_{r} (x)$ and $m_{r} (x)$ in $R$ , so the infimum and supremum over $r$ are taken in the ordered field and the elementary leastness arguments of steps 1.1--1.4 apply directly. For unbounded $u$ the envelopes can be infinite; idempotence in that setting must use the same local formulas extended to extended-valued inputs, whereas the present statement and Upper and lower semicontinuous envelopes by local limsup and liminf take real-valued input.
Strictness is not needed. The proof nowhere requires the contact or the majorant to be strict: the least-majorant property is proved by a direct pointwise comparison against an arbitrary upper semicontinuous majorant.

Depends on

Used by

Discontinuous viscosity solutions through the two envelopes Definition
Half-relaxed limits of a locally bounded family Definition

Dependency tree · two levels

15 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

Michael G. Crandall, Hitoshi Ishii and Pierre-Louis Lions, User's guide to viscosity solutions of second order partial differential equations, Bulletin of the American Mathematical Society 27 (1992), 1--67 (complete article) (standard reference, not scraped)
Hung Vinh Tran, Hamilton--Jacobi Equations: Theory and Applications, 2020 preliminary author manuscript of AMS Graduate Studies in Mathematics 213 (complete text) (standard reference, not scraped)