Energy estimates for a first-order operator on the line

For a continuously differentiable family of operators A(s) on a real inner product space, symmetric wherever the path is nonzero, integration by parts gives

∫ ‖u' + A u‖² = ∫ ‖u'‖² + ∫ ‖A u‖² - ∫ ⟪u, A' u⟫.

We prove this identity for compactly supported C¹ paths, without a finite-dimensionality or completeness assumption on the target. A spectral gap for A and a small upper bound on the quadratic form of A' give a coercive estimate. A second integration by parts, against a C¹ family S(s) of symmetric operators, gives

∫ ⟪S (u' + A u), u⟫ = ∫ ⟪S A u, u⟫ - ½ ∫ ⟪S' u, u⟫

for any continuous family A, with no symmetry of A assumed (TauCeti.integral_inner_apply_deriv_add_eq). When ⟪S A v, v⟫ - ½ ⟪S' v, v⟫ is coercive outside a set I and bounded below on I, this controls ∫ ‖u‖² by ∫ ‖u' + A u‖² and ∫_I ‖u‖² (TauCeti.half_mul_integral_norm_sq_le); ∫ ‖u'‖² is then controlled by TauCeti.integral_norm_deriv_sq_le. Global estimates with an interior error and coercivity outside a compact interval are developed in EnergyEstimate.Global. These estimates for bounded coefficients are inputs to the Fredholm property of d/ds + A(s); they do not assert surjectivity or the Fredholm property, nor treat unbounded transverse operators on a strip.

References

• D. McDuff and D. Salamon, J-holomorphic Curves and Symplectic Topology, 2nd ed., Appendix A (first-order Fredholm operators).
• M. Schwarz, Morse Homology, Chapter 2 (linearized trajectory operators).

theorem TauCeti.integrable_norm_apply_sq_and_inner_deriv_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {A : ℝ → E →L[ℝ] E} {u : ℝ → E} (hA : ContDiff ℝ 1 A) (hu : Continuous u) (hc : HasCompactSupport u) : MeasureTheory.Integrable (fun (s : ℝ) => ‖(A s) (u s)‖ ^ 2) MeasureTheory.volume ∧ MeasureTheory.Integrable (fun (s : ℝ) => inner ℝ (u s) ((deriv A s) (u s))) MeasureTheory.volume

The squared coefficient norm and coefficient-derivative quadratic form are integrable along a compactly supported continuous path.

theorem TauCeti.integral_norm_deriv_add_sq_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {A : ℝ → E →L[ℝ] E} {u : ℝ → E} (hA : ContDiff ℝ 1 A) (hsym : ∀ s ∈ Function.support u, (↑(A s)).IsSymmetric) (hu : ContDiff ℝ 1 u) (hc : HasCompactSupport u) : ∫ (s : ℝ), ‖deriv u s + (A s) (u s)‖ ^ 2 = ((∫ (s : ℝ), ‖deriv u s‖ ^ 2) + ∫ (s : ℝ), ‖(A s) (u s)‖ ^ 2) - ∫ (s : ℝ), inner ℝ (u s) ((deriv A s) (u s))

The energy identity for d/ds + A(s). The coefficient derivative contributes with a minus sign. Symmetry is needed only on the support of the path, and is not assumed separately for the coefficient derivative.

theorem TauCeti.integrable_inner_apply_of_hasCompactSupport {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u : ℝ → E} {T : ℝ → E →L[ℝ] E} {w : ℝ → E} (hT : Continuous T) (hw : Continuous w) (hu : Continuous u) (hc : HasCompactSupport u) : MeasureTheory.Integrable (fun (s : ℝ) => inner ℝ ((T s) (w s)) (u s)) MeasureTheory.volume

The integrand ⟪T w, u⟫ is integrable when T and w are continuous and u is a compactly supported continuous path.

theorem TauCeti.integral_inner_apply_deriv_add_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {A : ℝ → E →L[ℝ] E} {u : ℝ → E} {S : ℝ → E →L[ℝ] E} (hS : ContDiff ℝ 1 S) (hsym : ∀ (s : ℝ), (↑(S s)).IsSymmetric) (hA : Continuous A) (hu : ContDiff ℝ 1 u) (hc : HasCompactSupport u) : ∫ (s : ℝ), inner ℝ ((S s) (deriv u s + (A s) (u s))) (u s) = (∫ (s : ℝ), inner ℝ ((S s) ((A s) (u s))) (u s)) - (∫ (s : ℝ), inner ℝ ((deriv S s) (u s)) (u s)) / 2

Integration by parts against a family of quadratic forms. For a C¹ family S of symmetric operators, a continuous family A and a compactly supported C¹ path u,

∫ ⟪S (u' + A u), u⟫ = ∫ ⟪S A u, u⟫ - ½ ∫ ⟪S' u, u⟫.

theorem TauCeti.half_mul_integral_norm_sq_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {A : ℝ → E →L[ℝ] E} {u : ℝ → E} {S : ℝ → E →L[ℝ] E} (hS : ContDiff ℝ 1 S) (hsym : ∀ (s : ℝ), (↑(S s)).IsSymmetric) (hA : Continuous A) (hu : ContDiff ℝ 1 u) (hc : HasCompactSupport u) {I : Set ℝ} (hI : MeasurableSet I) {c M K : ℝ} (hc0 : 0 < c) (hM : ∀ (s : ℝ), ‖S s‖ ≤ M) (hout : ∀ s ∉ I, ∀ (v : E), c * ‖v‖ ^ 2 ≤ inner ℝ ((S s) ((A s) v)) v - inner ℝ ((deriv S s) v) v / 2) (hin : ∀ s ∈ I, ∀ (v : E), -K * ‖v‖ ^ 2 ≤ inner ℝ ((S s) ((A s) v)) v - inner ℝ ((deriv S s) v) v / 2) : c / 2 * ∫ (s : ℝ), ‖u s‖ ^ 2 ≤ (M ^ 2 / (2 * c) * ∫ (s : ℝ), ‖deriv u s + (A s) (u s)‖ ^ 2) + (K + c) * ∫ (s : ℝ) in I, ‖u s‖ ^ 2

The estimate given by a family of quadratic forms: if ⟪S A v, v⟫ - ½ ⟪S' v, v⟫ is at least c ‖v‖² outside a set I and at least -K ‖v‖² on I, and ‖S‖ ≤ M, then c/2 ∫ ‖u‖² ≤ M²/(2c) ∫ ‖u' + A u‖² + (K + c) ∫_I ‖u‖².

theorem TauCeti.integral_norm_deriv_sq_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {A : ℝ → E →L[ℝ] E} {u : ℝ → E} (hA : Continuous A) (hu : ContDiff ℝ 1 u) (hc : HasCompactSupport u) {M : ℝ} (hM : ∀ (s : ℝ), ‖A s‖ ≤ M) : ∫ (s : ℝ), ‖deriv u s‖ ^ 2 ≤ (2 * ∫ (s : ℝ), ‖deriv u s + (A s) (u s)‖ ^ 2) + 2 * M ^ 2 * ∫ (s : ℝ), ‖u s‖ ^ 2

The derivative of a compactly supported C¹ path is controlled by u' + A u and u: ∫ ‖u'‖² ≤ 2 ∫ ‖u' + A u‖² + 2 M² ∫ ‖u‖² when ‖A s‖ ≤ M everywhere.

theorem TauCeti.integral_norm_deriv_sq_add_mul_integral_norm_sq_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {A : ℝ → E →L[ℝ] E} {u : ℝ → E} (hA : ContDiff ℝ 1 A) (hsym : ∀ s ∈ Function.support u, (↑(A s)).IsSymmetric) (hu : ContDiff ℝ 1 u) (hc : HasCompactSupport u) {α β : ℝ} (hα : 0 ≤ α) (hgap : ∀ s ∈ Function.support u, α * ‖u s‖ ≤ ‖(A s) (u s)‖) (hsmall : ∀ s ∈ Function.support u, inner ℝ (u s) ((deriv A s) (u s)) ≤ β * ‖u s‖ ^ 2) : (∫ (s : ℝ), ‖deriv u s‖ ^ 2) + (α ^ 2 - β) * ∫ (s : ℝ), ‖u s‖ ^ 2 ≤ ∫ (s : ℝ), ‖deriv u s + (A s) (u s)‖ ^ 2

A spectral gap and a bound on the coefficient derivative give a coercive estimate for a compactly supported path. Symmetry and both bounds need hold only where the path is nonzero. The estimate is useful when β < α², but is valid without that extra hypothesis.