PropositionStatement: 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.

Proposition 4.6: conditional adjoint observability

PDF p. 19: Proposition 4.6; (4.5)

Statement

Assume the Axiom of Choice and hypotheses (H), (W), and (UCPw). Thus $n \geq 2$ , $Ω = R^{n} ∖ Θ$ is the connected exterior of a nonempty compact smooth nontrapping obstacle, $T > 0$ , and $w \in C ([0, T]; H_{D}^{2} (Ω) \cap W^{2, \infty} (Ω))$ is the reference solution specified in Reference trajectory hypothesis W. The hypothesis (UCPw) is the energy-level unique continuation implication in Conditional energy-level unique continuation hypothesis for this trajectory and the observation region $ω = {x \in Ω : ∣ x ∣ > R}$ .

Let $H_{D}^{σ} (Ω)$ be the Dirichlet spectral scale and $U (t)$ the real-linear adjoint evolution for $i v_{t} + Δ_{D} v + 2 λ ∣ w ∣^{2} v - λ w^{2} \overline{v} = 0$ , with $λ \in R ∖ {0}$ . Let $φ$ be the real cutoff of Control region and nested real cutoffs, positive exactly on $ω$ . For each $σ \in {- 1, - 2}$ there is a constant $C > 0$ , depending on the fixed data and $σ$ but not on $v_{0}$ , such that every $v_{0} \in H_{D}^{σ} (Ω)$ satisfies

$∥ v_{0} ∥_{H_{D}^{σ}}^{2} \leq C \int_{0}^{T} ∥ φ U (t) v_{0} ∥_{H_{D}^{σ}}^{2} d t .$

Facts & Assumptions

[F1]

The geometry, nontrapping condition, trajectory, spectral scale and cutoffs are specified by Exterior and truncated obstacle domains, Non-trapping obstacle, Reference trajectory hypothesis W, Dirichlet spectral Sobolev scale and duality and Control region and nested real cutoffs. The scale is a complex Hilbert space at each index; $R_{D} = (I - Δ_{D})^{- 1}$ maps $H_{D}^{σ}$ isometrically to $H_{D}^{σ + 2}$ . Choice is assumed as in The Axiom of Choice.

[F2]

The evolution $U (t)$ is bounded and real-linear on $H_{D}^{σ}$ , uniformly for $t \in [0, T]$ , and its trajectories are norm-continuous Forward and backward real-linear propagators. Multiplication by $φ$ is bounded on the relevant scale Cutoff multipliers through order two and by duality. The regularized trajectory is $R_{D} U (t) v_{0}$ Resolvent-regularized adjoint and its forcing.

[F3]

Under these hypotheses Lemma 4.3: perturbed observability modulo a remainder bounds the squared initial norm by a fixed multiple of the sum of the observation integral in the statement and $\int_{0}^{T} ∥ ψ R_{D} U (t) v_{0} ∥_{2}^{2} d t$ , where $ψ$ is the compact cutoff of Control region and nested real cutoffs. If initial data converge weakly in $H_{D}^{σ}$ , Lemma 4.4: compactness for regularized perturbed trajectories gives strong convergence of their localized regularized trajectories in $L^{2} (0, T; L^{2} (Ω))$ .

[F4]

If $φ U (t) v_{0} = 0$ in $H_{D}^{σ}$ for every $t \in [0, T]$ , Lemma 4.5: invisible solutions acquire energy regularity gives $U (\cdot) v_{0} \in C ([0, T]; H_{0}^{1} (Ω))$ . The hypothesis Conditional energy-level unique continuation hypothesis says that an energy-level adjoint solution vanishing almost everywhere on $(0, T) \times ω$ is identically zero.

[F5]

Under Countable Choice, a real or complex Hilbert space is reflexive Hilbert spaces are reflexive. Under the ultrafilter lemma, dependent choice and Hahn–Banach, every bounded sequence in a reflexive Banach space has a weakly convergent subsequence Reflexivity is equivalent to weak subsequential compactness of bounded sequences. The assumed full Choice implies dependent choice and countable choice by AC implies DC implies countable choice, the filter-extension form of the ultrafilter lemma by The ultrafilter lemma, from the Axiom of Choice: every filter extends to an ultrafilter, and the real dominated-extension principle HB by Hahn-Banach dominated extension theorem for real vector spaces. These are exactly the choice hypotheses of the two preceding suppliers.

[F6]

The spaces $C ([0, T]; X)$ and $L^{2} (0, T; X)$ use the norm-continuous-path and Bochner time-space conventions of Continuous and mixed time-space function spaces. Weak convergence under all bounded scalar-linear functionals and realification with the unchanged norm are defined in Weak convergence notation in normed state spaces.

Proof

Given: The fixed data and hypotheses in the Statement, and $σ \in {- 1, - 2}$ .

Goal: Prove the displayed observability estimate for every datum in $H_{D}^{σ}$ .

1.1F1F2F5F6givenassume-contra

Suppose the estimate fails. For each positive integer $j$ , choose a nonzero datum and normalize it to obtain $v_{j, 0} \in H_{D}^{σ}$ with $∥ v_{j, 0} ∥_{H_{D}^{σ}} = 1$ and $\int_{0}^{T} ∥ φ U (t) v_{j, 0} ∥_{H_{D}^{σ}}^{2} d t < 1 / j$ . Normalization uses real homogeneity of $U (t)$ . By the Hilbert-space weak subsequence result, after passing to a subsequence, $v_{j, 0} ⇀ v_{0}$ in $H_{D}^{σ}$ .

2.1F2F6step 1.1

Define $O a = φ U (\cdot) a$ as a map from the realification of $H_{D}^{σ}$ into $L^{2} (0, T; H_{D}^{σ})$ , also regarded as real. The uniform evolution and multiplier bounds make $O$ bounded and real-linear. Complex weak convergence implies weak convergence in the realification, since each bounded real-linear functional is the real part of a bounded complex-linear functional. Consequently $O v_{j, 0}$ converges weakly to $O v_{0}$ . Its norms tend to zero by step 1.1, so $O v_{0} = 0$ . Norm-continuity of $t \mapsto φ U (t) v_{0}$ then gives $φ U (t) v_{0} = 0$ in $H_{D}^{σ}$ for every $t \in [0, T]$ .

3.1F1F2F4step 2.1

The invisible-solution lemma gives $U (\cdot) v_{0} \in C ([0, T]; H_{0}^{1} (Ω))$ . Since $φ$ is smooth and strictly positive on $ω$ , the distributional equality $φ U (t) v_{0} = 0$ implies $U (t) v_{0} = 0$ on $ω$ : locally divide a compactly supported test function by $φ$ . The energy-level trajectory therefore vanishes almost everywhere on $(0, T) \times ω$ . Its adjoint equation and continuity meet the hypotheses of (UCPw), which yields $U (\cdot) v_{0} = 0$ and hence $v_{0} = 0$ .

4.1F3step 1.1step 3.1discharge-contradiction∎

The compactness lemma now gives $ψ R_{D} U (\cdot) v_{j, 0} \to 0$ strongly in $L^{2} (0, T; L^{2} (Ω))$ . Applying the observability estimate with remainder to each $v_{j, 0}$ makes its right-hand side tend to zero: the observation term tends to zero by step 1.1, and the remainder tends to zero by the preceding strong convergence. Thus $∥ v_{j, 0} ∥_{H_{D}^{σ}}^{2} \to 0$ , contradicting its value $1$ . The failure assumption is impossible, proving the stated estimate.

Source notes

The article is cited for attribution of Proposition 4.6 and its compactness–uniqueness strategy. The deduction above uses the stated suppliers, not the proposition as its own premise. The explicit Choice assumption records hypotheses of the suppliers and is not attributed to the article.

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 page 19, Proposition 4.6 and equation (4.5)