The bounded first-order trajectory operator #
The operator D_A = d/ds + A(s) acts from the first-order weak-derivative graph to Lᵖ
for any essentially bounded, strongly measurable family of bounded operators on a real Banach
space. We use the existing WeakDerivStep over the identity map on Lᵖ, so its norm controls
both the value and its weak derivative. No new Sobolev carrier is introduced.
WeakDerivStep.trajectoryOperator is a continuous linear map. Its operator norm is at most
1 + ‖A‖, and changing the coefficient changes the operator by at most the L∞ distance
between coefficients. Solving D_A u = f is equivalent to the weak ordinary differential
equation u' = f - A u. For differentiable representatives with locally integrable derivative,
the operator agrees almost everywhere with the classical expression u' + A u. In particular,
for a path in W^{1,2}(ℝ, F) with a C¹ representative φ, the squared norms of the path, of
its weak derivative and of its image under D_A are ∫ ‖φ‖², ∫ ‖φ'‖² and ∫ ‖φ' + A φ‖²
(TauCeti.WeakDerivStep.norm_prev_sq_eq_integral,
TauCeti.WeakDerivStep.norm_weakFDeriv_sq_eq_integral and
TauCeti.WeakDerivStep.norm_trajectoryOperator_sq_eq_integral).
On the line, for a path with a C¹ representative φ, the squared norm of D_A u is the
integral of ‖φ' + A φ‖² (TauCeti.WeakDerivStep.norm_trajectoryOperator_sq_eq_integral).
These statements supply the bounded realization to which coercive estimates and compact-error criteria can be applied. They do not assert Fredholmness, asymptotic invertibility, or density of smooth paths. Neither symmetry nor finite dimensionality of the target is required.
References #
- D. McDuff and D. Salamon, J-holomorphic Curves and Symplectic Topology, 2nd ed., Appendix A.1 (first-order Fredholm operators).
- M. Schwarz, Morse Homology, Chapter 2 (linearized trajectory operators).
The coefficient action is Mathlib's ContinuousLinearMap.holderL, applied to evaluation;
the domain is the closed weak-derivative graph of TauCeti.Analysis.Sobolev.GraphStep.Basic.
The first-order operator u ↦ u' + A u on the weak-derivative graph over Lᵖ.
The coefficient is an L∞ operator field, so the definition depends only on its almost
everywhere equivalence class.
Instances For
The operator is the sum of the weak derivative in direction 1 and the coefficient action.
On representatives, the bounded trajectory operator has the expected pointwise formula almost everywhere.
The operator norm of the first-order trajectory operator is at most 1 + ‖A‖.
The weak derivative of a path is controlled by its image under the trajectory operator and
its Lᵖ norm: ‖u'‖ ≤ ‖u' + A u‖ + ‖A‖ ‖u‖.
Subtracting two trajectory operators cancels the derivative part and leaves multiplication by the difference of their coefficients.
An L∞ perturbation of the coefficient changes the trajectory operator by at most the same
amount in operator norm.
The trajectory operator depends 1-Lipschitz continuously on its L∞ coefficient, for the
operator norm.
Solving the bounded trajectory equation is equivalent to solving the weak ordinary
differential equation u' = f - A u.
Weak solutions are values of graph elements. If an Lᵖ path x has weak derivative
f - A x, then x is the value of an element u of the weak-derivative graph with
D_A u = f. This is the converse of trajectoryOperator_eq_iff_hasWeakLineDerivOn: there the
element u is given, here it is constructed from x.
For a differentiable representative whose derivative is locally integrable, the Sobolev
trajectory operator agrees almost everywhere with the classical expression v' + A v.
Norms of a path with a C¹ representative #
On a path with a C¹ representative φ, the squared norm of D_A is
∫ ‖φ' + A φ‖².