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 3.10: order-two local control
PDF p. 16: Proposition 3.10
Statement
Assume the Axiom of Choice and (H): , the nonempty compact obstacle has smooth boundary and connected exterior , and its generalized reflected rays leave every compact set in finite time. Let , and . Let be the control cutoff of Control region and nested real cutoffs. Put and with its supremum norm. The space is the order-two Dirichlet spectral space; it equals with equivalent norms, where is the closure of compactly supported smooth functions.
The three hypotheses of Abstract nonlinear control-space hypotheses hold at for this . Consequently there is such that any with both spectral norms at most can be joined by an integral solution of , with , and a control . Thus the system is locally exactly controllable in ; equivalence of norms allows the smallness condition to be expressed in the ordinary norm. The integral solution is understood through the variation-of-constants formulation in Mild formulation of the controlled power NLS, with .
Facts & Assumptions
The geometry and cutoff are those of Exterior and truncated obstacle domains and Control region and nested real cutoffs. The spectral scale Dirichlet spectral Sobolev scale and duality is complete, and Exterior H2 algebra and polynomial nonlinear estimates identifies with with equivalent norms. The weak Sobolev and closure conventions are those of Complex integer-order Sobolev notation.
Under Choice, Scale isometries and free Schrödinger evolution gives a strongly continuous unitary group on . Choice is assumed as in The Axiom of Choice.
Exterior H2 algebra and polynomial nonlinear estimates gives, for and , Bochner-integrability of and the bounds and .
Continuous and mixed time-space function spaces fixes norm-continuous paths, strongly measurable Bochner functions and their norms. The Bochner integrability criterion, integral norm bound and commutation with bounded linear operators are supplied by Bochner integrability criterion, Bochner integral norm inequality and Bounded linear maps commute with Bochner integration. Scalar integrals of integrable functions are absolutely continuous by Absolute continuity of the integral.
If (Y,d) is complete then Y^X is complete in the uniform metric, and so is C(X,Y) gives completeness of the continuous-function space for a complete target in the uniform metric. Abstract nonlinear control-space hypotheses specifies the three bounds required for the application of Theorem 3.7: abstract small-data perturbation result.
Mild formulation of the controlled power NLS specifies the integral-solution concept and its equivalent variation-of-constants formulation on ; here , with the same assumed Choice principle, free group, nonlinearity and control force.
Proof
Given: The assumptions, spaces and parameters in the Statement.
Goal: Verify the three abstract perturbation hypotheses and apply the nonlinear control theorem.
The target is complete by F1. F5 makes the continuous path space complete in the truncated uniform metric; for distances below one that metric agrees with the supremum distance. Hence every supremum-norm Cauchy sequence converges in supremum norm. With the pointwise vector operations and supremum norm of F4, is a Banach space. Its inclusion into is the identity and has norm one.
Let . Strong measurability of follows by approximating almost everywhere by finite-range measurable functions: for each fixed value, is continuous, and its restriction to the compact interval is a uniform limit of finite-range measurable functions. Unitarity preserves the norm, so F4 gives its Bochner integrability. Set . The integral norm bound gives , so F4 makes continuous. Strong continuity and unitarity imply that is continuous: split its increment into and .
By F2, is a continuous -valued path and . This proves the homogeneous hypothesis.
By the group law and commutation of a bounded linear map with the Bochner integral, . The integral norm bound and unitarity give . This proves the retarded-forcing hypothesis, including existence and path continuity.
F3 gives the required nonlinear membership and both power bounds. Taking one constant large enough for the constants in steps 2.1 and 2.2 and F3 verifies all three conditions of F5 for the same .
The dimension, geometry, time, exponent, coefficient and cutoff meet the hypotheses of Theorem 3.7: abstract small-data perturbation result, and lies in its stated range. Applying it with the space verified in step 3.1 gives the stated , control and integral solution with the prescribed endpoints. The identification and norm equivalence in F1 give the stated formulation in and permit an ordinary- smallness radius. This proves the proposition.
Source notes
The frozen article is cited for attribution of Proposition 3.10. The deduction uses the separately stated control theorem and its mathematical prerequisites; the article is not used as a proof of those prerequisites.
Depends on
- Exterior and truncated obstacle domains
- Control region and nested real cutoffs
- Dirichlet spectral Sobolev scale and duality
- Abstract nonlinear control-space hypotheses
- Complex integer-order Sobolev notation
- Continuous and mixed time-space function spaces
- Theorem 3.7: abstract small-data perturbation result
- Exterior H2 algebra and polynomial nonlinear estimates
- Scale isometries and free Schrödinger evolution
- Mild formulation of the controlled power NLS
- The Axiom of Choice
- If (Y,d) is complete then Y^X is complete in the uniform metric, and so is C(X,Y)
- Bochner integrability criterion
- Bochner integral norm inequality
- Bounded linear maps commute with Bochner integration
- Absolute continuity of the integral
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 16, Proposition 3.10