Variations of a curve with fixed endpoints

A variation of a curve γ : ℝ → M is a two-parameter family F : ℝ → ℝ → M with F 0 = γ, whose first argument is the variation parameter s and whose second argument is the curve parameter t. Its variation field TauCeti.Manifold.variationField I F is the transverse velocity V(t) = ∂F/∂s (0, t).

This file names the variations against which a curve between the parameters a and b is compared with nearby curves joining the same two points: TauCeti.Manifold.IsFixedEndpointVariation I n F a b says that the uncurried family is C^n at every point of {0} × [a, b] and that, for s near 0, the curve F s has the same endpoints F 0 a and F 0 b as the central curve. The variation field of such a variation vanishes at both endpoints.

These are the variations of the first variation formula and of the critical points of the energy (TauCeti.Geometry.Manifold.Riemannian.FirstVariation.Basic). The definition uses only the manifold structure, not a metric; [a, b] is the unordered interval Set.uIcc a b.

Main definitions and results

• TauCeti.Manifold.IsFixedEndpointVariation: a two-parameter family is a C^n variation of its central curve with fixed endpoints.
• TauCeti.Manifold.IsFixedEndpointVariation.contMDiffAt_apply_zero: the central curve of a C^n fixed-endpoint variation is C^n on [a, b].
• TauCeti.Manifold.IsFixedEndpointVariation.variationField_left_eq_zero and TauCeti.Manifold.IsFixedEndpointVariation.variationField_right_eq_zero: the variation field vanishes at the endpoints.
• TauCeti.Manifold.isFixedEndpointVariation_const_iff: the constant family at a curve γ is a C^n fixed-endpoint variation exactly when γ is C^n on [a, b].

References

• M. P. do Carmo, Riemannian Geometry, Birkhäuser, 1992, Ch. 9, §2, Definition 2.1 (proper variations).
• J. M. Lee, Introduction to Riemannian Manifolds, GTM 176, 2nd ed., 2018, Ch. 6, variations of curves and proper variations.

structure TauCeti.Manifold.IsFixedEndpointVariation {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] (n : WithTop ℕ∞) (F : ℝ → ℝ → M) (a b : ℝ) : Prop

A two-parameter family F : ℝ → ℝ → M is a C^n variation with fixed endpoints of its central curve F 0 between the parameters a and b when the uncurried family (s, t) ↦ F s t is C^n at every point of {0} × [a, b] and, for s near 0, the curve F s passes through F 0 a at a and through F 0 b at b.

• contMDiffAt (t : ℝ) : t ∈ Set.uIcc a b → ContMDiffAt (modelWithCornersSelf ℝ (ℝ × ℝ)) I n (fun (z : ℝ × ℝ) => F z.1 z.2) (0, t)

  A fixed-endpoint variation is C^n at every point of {0} × [a, b].

• eventually_apply_left : ∀ᶠ (s : ℝ) in nhds 0, F s a = F 0 a

  Near s = 0, the curves of a fixed-endpoint variation start at F 0 a.

• eventually_apply_right : ∀ᶠ (s : ℝ) in nhds 0, F s b = F 0 b

  Near s = 0, the curves of a fixed-endpoint variation end at F 0 b.

theorem TauCeti.Manifold.IsFixedEndpointVariation.of_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {m n : WithTop ℕ∞} {F : ℝ → ℝ → M} {a b : ℝ} (h : IsFixedEndpointVariation I n F a b) (hmn : m ≤ n) : IsFixedEndpointVariation I m F a b

A C^n fixed-endpoint variation is a C^m fixed-endpoint variation for every m ≤ n.

theorem TauCeti.Manifold.IsFixedEndpointVariation.contMDiffAt_apply_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} {F : ℝ → ℝ → M} {a b : ℝ} (h : IsFixedEndpointVariation I n F a b) {t : ℝ} (ht : t ∈ Set.uIcc a b) : ContMDiffAt (modelWithCornersSelf ℝ ℝ) I n (F 0) t

The central curve of a C^n fixed-endpoint variation is C^n at every point of [a, b].

theorem TauCeti.Manifold.IsFixedEndpointVariation.variationField_left_eq_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} {F : ℝ → ℝ → M} {a b : ℝ} (h : IsFixedEndpointVariation I n F a b) : variationField I F a = 0

The variation field of a fixed-endpoint variation vanishes at the left endpoint.

theorem TauCeti.Manifold.IsFixedEndpointVariation.variationField_right_eq_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} {F : ℝ → ℝ → M} {a b : ℝ} (h : IsFixedEndpointVariation I n F a b) : variationField I F b = 0

The variation field of a fixed-endpoint variation vanishes at the right endpoint.

@[simp]

theorem TauCeti.Manifold.isFixedEndpointVariation_const_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} {a b : ℝ} {γ : ℝ → M} : IsFixedEndpointVariation I n (fun (x : ℝ) => γ) a b ↔ ∀ t ∈ Set.uIcc a b, ContMDiffAt (modelWithCornersSelf ℝ ℝ) I n γ t

The trivial variation. The constant family at a curve γ is a C^n variation of γ with fixed endpoints between a and b exactly when γ is C^n at every point of [a, b].