TheoremStatement: Literature-sourcedProof: AI-generated

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.

Theorem 1.1: exact outer boundary controllability

PDF p. 4: Theorem 1.1; (1.7); PDF p. 16: proof begins; PDF p. 17: proof concludes

Statement

Assume the Axiom of Choice. Let $n \in {2, 3}$ and let $Θ \subset R^{n}$ be a nonempty compact obstacle with smooth boundary, connected exterior $Ω = R^{n} ∖ Θ$ , and non-trapping generalized reflected and glancing rays: each such ray leaves every compact set in finite forward time. Choose $R_{0} > 0$ with $Θ \subset B_{R_{0}} (0)$ and set $Ω_{0} = B_{R_{0}} (0) ∖ Θ$ , $Γ_{1} = \partial B_{R_{0}} (0)$ and $Γ_{2} = \partial Θ$ .

Let $T > 0$ , $s \in {1, 2}$ and $λ \in R ∖ {0}$ . Write $X^{s} (Ω_{0}) = {f \in H^{s} (Ω_{0}) : γ_{Γ_{2}} f = 0}$ , with the inherited $H^{s}$ norm; $γ$ denotes the Sobolev value trace. Then there is $δ > 0$ such that, for every $u_{0}, u_{1} \in X^{s} (Ω_{0})$ with $∥ u_{0} ∥_{H^{s}}, ∥ u_{1} ∥_{H^{s}} \leq δ$ , there are $u \in C ([0, T]; H^{s} (Ω_{0}))$ and $h \in C ([0, T]; H^{s - 1 / 2} (Γ_{1}))$ satisfying

$i \partial_{t} u + Δ u + λ ∣ u ∣^{2} u = 0 in D^{'} ((0, T) \times Ω_{0}),$

with $u (0) = u_{0}$ , $u (T) = u_{1}$ , $γ_{Γ_{1}} u = h$ , and $γ_{Γ_{2}} u = 0$ . The boundary equalities are Sobolev trace equalities at every time, and $C ([0, T]; Y)$ means norm-continuous paths in $Y$ .

Statement references

Exterior and truncated obstacle domains

Non-trapping obstacle

States compatible with the uncontrolled obstacle boundary

Cubic NLS and boundary control formulations

Continuous and mixed time-space function spaces

Distributional equation convention for complex Schrödinger solutions

The Axiom of Choice

Facts & Assumptions

[F1]

The geometry and non-trapping convention are those of Exterior and truncated obstacle domains and Non-trapping obstacle. The state space and trace convention are those of States compatible with the uncontrolled obstacle boundary, the boundary equation is that of Cubic NLS and boundary control formulations, and time continuity and distributional equality have the meanings in Continuous and mixed time-space function spaces and Distributional equation convention for complex Schrödinger solutions. The assumed choice principle is The Axiom of Choice.

[F2]

Under these geometric and Choice hypotheses, Lemma 3.11: extension preserving the obstacle Dirichlet condition supplies a bounded linear extension $E : X^{s} (Ω_{0}) \to H_{D}^{s} (Ω)$ with $(E f) ∣_{Ω_{0}} = f$ . Here Dirichlet spectral Sobolev scale and duality defines $H_{D}^{s} (Ω) = D ((I - Δ_{D})^{s / 2})$ with its spectral norm, and Low-order identifications of the Dirichlet scale identifies it with $H^{s} (Ω) \cap H_{0}^{1} (Ω)$ for the present $s$ , with equivalent norms.

[F3]

For $R = R_{0} + 1$ , Control region and nested real cutoffs supplies a smooth cutoff $φ$ equal to zero on $∣ x ∣ \leq R$ , positive on $∣ x ∣ > R$ , and one on $∣ x ∣ \geq R + 1$ . With this cutoff and $m = 3$ , Theorem 1.3: cubic internal control near zero gives a positive exterior endpoint radius and an integral solution and control continuous in $H_{D}^{s}$ for every pair of exterior endpoints inside that radius. The controlled equation is specified by Linear and nonlinear internally controlled exterior systems.

[F4]

The integral-solution convention in Mild formulation of the controlled power NLS requires $g (v) = λ ∣ v ∣^{2} v$ and $φ k$ to be Bochner integrable in $X = H_{D}^{s} (Ω)$ . Writing $f = i g (v) - i φ k$ , $B$ for the generator on $X$ , and $q_{X} (t) = \int_{0}^{t} v (r) d r$ , it gives $q_{X} (t) \in D (B)$ and $v (t) = v (0) + B q_{X} (t) + \int_{0}^{t} f (r) d r$ . The group on $X$ is the consistent extension of $W (t) = e^{i t Δ_{D}}$ on $L^{2} (Ω)$ by Scale isometries and free Schrödinger evolution.

[F5]

The Dirichlet realization in Dirichlet Laplacian and positive shift is self-adjoint on $L^{2} (Ω)$ , with $D (Δ_{D}) = H^{2} (Ω) \cap H_{0}^{1} (Ω)$ , and its action there is the weak spatial Laplacian. Since $A = I - Δ_{D} \geq I$ , the spectral norm in Dirichlet spectral Sobolev scale and duality gives the bounded inclusion $J : X \to L^{2} (Ω)$ : $∥ J w ∥_{2} \leq ∥ w ∥_{X}$ . For this self-adjoint $Δ_{D}$ , Flow calculus of a self-adjoint generator: commutation, invariance and differentiability, part (a), identifies the full $L^{2}$ generator domain of $W$ with $D (Δ_{D})$ and the generator with $i Δ_{D}$ . That supplier has domain mathematics, assumes AC and Countable Choice, and uses no physical premise; both choice hypotheses follow from the assumed AC.

[F6]

On the smooth bounded truncated domain $Ω_{0}$ , Collar traces and extension across an artificial boundary supplies the bounded trace $H^{1} (Ω_{0}) \to H^{1 / 2} (Γ_{2})$ , agreeing with classical restriction on smooth functions. Its traces at orders $1 \leq s \leq 2$ agree in $L^{2} (Γ_{2})$ with this first-order trace and are local, so restriction from an exterior collar gives the same obstacle trace.

[F7]

Bounded linear maps commute with Bochner integration applies to the bounded inclusion $J$ and to bounded spatial test functionals on $L^{2}$ . Holder's inequality for integrals, including the endpoint cases, applied to absolute values with exponents $2, 2$ , gives $∥ a ∥_{L^{1} (K)} \leq ∣ K ∣^{1 / 2} ∥ a ∥_{2}$ on every spatial set $K$ of finite measure. Fubini's theorem for L¹ functions on a sigma-finite product permits exchanging the integrals of absolutely integrable complex functions on the Lebesgue time and space products used below. The time interval is finite, spatial test supports are compact, and these measures are sigma-finite.

[F8]

Transfer from exterior internal control to outer boundary control transfers an exterior solution satisfying the distributional equation, local integrability and zero obstacle trace, together with its endpoint values and outer trace, to the stated boundary problem when the cutoff vanishes on $Ω_{0}$ .

Proof

Given: The hypotheses and endpoint data in the Statement.

Goal: Construct a boundary control and a solution with the prescribed endpoints, equation and traces.

1.1F2F3given

Choose $R = R_{0} + 1$ and the cutoff in F3. Let $δ_{1} > 0$ be the radius supplied there, and let $E$ be the extension in F2. The operator norm $∥ E ∥$ is positive: a nonzero smooth function compactly supported in $Ω_{0}$ belongs to $X^{s} (Ω_{0})$ and is recovered by restriction after applying $E$ . Set $δ = δ_{1} / ∥ E ∥$ . Then $∥ E u_{j} ∥_{H_{D}^{s}} \leq δ_{1}$ for $j = 0, 1$ .

2.1F3F4F5F7step 1.1

Apply F3 to the extended endpoints. It supplies $k, v \in C ([0, T]; X)$ with $v (0) = E u_{0}$ and $v (T) = E u_{1}$ , where $X = H_{D}^{s} (Ω)$ , and the integral-solution identity in F4. Retain its notation $f = i λ ∣ v ∣^{2} v - i φ k$ and $q_{X} (t) = \int_{0}^{t} v (r) d r$ . In particular $g (v), φ k, f \in L^{1} (0, T; X)$ . By the inclusion $J$ and the local estimate in F7, their $L^{2}$ realizations, and also the continuous $L^{2}$ paths $v$ and $k$ , have jointly measurable, locally integrable space-time representatives. For example, for compact $K \subset Ω$ , $\int_{0}^{T} \int_{K} ∣ J f (t, x) ∣ d x d t \leq ∣ K ∣^{1 / 2} \int_{0}^{T} ∥ f (t) ∥_{X} d t$ . Jointly measurable local representatives can be obtained from Bochner simple approximations, which converge in local space-time $L^{1}$ by the same estimate.

3.1F4F5F7step 2.1

Fix $t$ and put $q (t) = J q_{X} (t) = \int_{0}^{t} J v (r) d r$ , where the equality is F7. Since $q_{X} (t) \in D (B)$ , its right group difference quotient converges in $X$ to $B q_{X} (t)$ . Applying $J$ and the consistency in F4 gives convergence of the same quotient in $L^{2}$ to $J B q_{X} (t)$ . For a unitary group a right limit is also the left limit: for $h > 0$ , $(W (- h) q - q) / (- h) = W (- h) (W (h) q - q) / h$ , and strong continuity preserves the limit. Thus the full generator identification in F5 gives $q (t) \in D (Δ_{D})$ and $J B q_{X} (t) = i Δ_{D} q (t)$ . Applying $J$ to the integral identity therefore yields $J v (t) = J v (0) + i Δ_{D} q (t) + p (t)$ in $L^{2}$ , where $p (t) = \int_{0}^{t} J f (r) d r$ . On this full domain, $Δ_{D} q (t) = Δ_{x} q (t)$ in spatial distributions by F5.

3.2F2F6step 2.1

Fix any $t \in [0, T]$ . By F2, $v (t) \in H_{0}^{1} (Ω)$ , so there are $w_{j} \in C_{c}^{\infty} (Ω)$ converging to $v (t)$ in $H^{1} (Ω)$ . Their restrictions converge to $v (t) ∣_{Ω_{0}}$ in $H^{1} (Ω_{0})$ : every whole-space $H^{1}$ representative of their difference from $v (t)$ on $Ω$ is also a representative on $Ω_{0}$ , so restriction cannot increase the quotient norm. Each $w_{j}$ vanishes near $Γ_{2}$ , so its classical trace there is zero. Boundedness of the first-order trace in F6 makes the $H^{1 / 2} (Γ_{2})$ trace of $v (t) ∣_{Ω_{0}}$ zero. Since $v (t) ∣_{Ω_{0}} \in H^{s} (Ω_{0})$ and the order- $s$ trace agrees in $L^{2}$ with that first-order trace, its $H^{s - 1 / 2} (Γ_{2})$ trace is zero as well. Trace locality identifies this with the exterior obstacle trace. This argument applies separately at every $t$ , including the endpoints, and requires no convergence of $w_{j}$ in $H^{2}$ .

4.1F1F5F7step 2.1step 3.1

The primitives in step 3.1 satisfy $\partial_{t} q = J v$ and $\partial_{t} p = J f$ in space-time distributions. Explicitly, for $a = J v$ or $a = J f$ , $P_{a} (t) = \int_{0}^{t} a (r) d r$ and arbitrary $η \in C_{c}^{\infty} ((0, T) \times Ω; C)$ , bounded spatial test functionals and Fubini give $\int_{0}^{T} \int_{Ω} P_{a} (t, x) \partial_{t} η (t, x) d x d t = \int_{0}^{T} \int_{Ω} a (r, x) (\int_{r}^{T} \partial_{t} η (t, x) d t) d x d r = - \int_{0}^{T} \int_{Ω} a (r, x) η (r, x) d x d r$ . Absolute integrability follows from the estimate in step 2.1, the finite time interval, and boundedness of the test function and its derivative. This calculation uses the bilinear distribution pairing, with no conjugation. The $L^{2}$ identity in step 3.1 also gives $Δ_{x} q = (J v - J v (0) - p) / i$ as a locally integrable space-time distribution. Differentiating that identity, commuting spatial and temporal distributional derivatives, and using the two primitive identities gives $\partial_{t} v = i Δ_{x} v + f$ . Multiplication by $i$ and the definition of $f$ give $i \partial_{t} v + Δ_{x} v + λ ∣ v ∣^{2} v = φ k$ in distributions. No assertion that $v (t)$ itself lies in $D (Δ_{D})$ is used.

5.1F1F8step 1.1step 2.1step 3.1step 4.1step 3.2∎

The cutoff vanishes on $Ω_{0}$ , since $R > R_{0}$ . Steps 2.1, 3.1, 3.2 and 4.1 verify local integrability, the exterior distributional equation and zero obstacle trace, so all hypotheses of the boundary-transfer proposition in F8 hold for $v, E$ and $m = 3$ . It gives $u = v ∣_{Ω_{0}}$ and $h = γ_{Γ_{1}} v$ with the asserted path regularity, endpoint values and boundary traces, and with the unforced cubic equation in distributions on $(0, T) \times Ω_{0}$ . These are precisely the conditions in the Statement.

Source notes

The frozen article is cited for attribution of Theorem 1.1 and its extension-and-restriction reduction. The proof above uses the separately supplied internal-control theorem, extension and transfer proposition; it does not use the article's boundary-control claim as a premise.

The integral-to-distribution and zero-trace bridges above are local arguments using the declared mathematical suppliers, including a Physics Library item whose actual domain is mathematics. The article citation is used only for original-theorem attribution; no prerequisite is imported from the article and no independent acceptance is claimed.

Depends on

Used by · 2

Dependency tree · 2 levels

Each result is drawn at its shortest distance from this item. Arrows run from prerequisites to the items that use them; this item has a heavier outline. External source nodes link directly to the cited text. The view shows up to two dependency steps; open a prerequisite to continue.

Sources

Nonlinear Schrödinger equation in an exterior domain, v2 · PDF pages 4 and 16–17, Theorem 1.1 and its proof