Chart variations of a curve

Let γ : ℝ → M be a curve, ψ = extChartAt I x₀ the extended chart at a point x₀, e a vector of the model space and φ : ℝ → ℝ a profile supported in a set J of parameters along which γ stays in the chart. The chart variation TauCeti.Manifold.chartVariation I γ x₀ J φ e is the two-parameter family (s, t) ↦ ψ⁻¹ (ψ (γ t) + (s φ(t)) • e), equal to γ t outside J: it pushes γ in the direction of the coordinate vector e, with profile φ.

These variations are the test variations of first variation arguments: a curve along which a functional is stationary for every chart variation satisfies the pointwise Euler–Lagrange equation. On a manifold without boundary the chart variation is as regular as γ, φ and the manifold, wherever the displaced points stay in the chart target, and its variation field is φ t times the tangent vector at γ t with coordinates e in the tangent-bundle trivialization at x₀.

Main definitions and results

• TauCeti.Manifold.chartVariation: the chart variation of a curve.
• TauCeti.Manifold.chartVariation_zero: its central curve is γ.
• TauCeti.Manifold.contMDiffAt_chartVariation: it is C^n at (s, t) when γ is C^n at t and the displaced point lies in the chart target.
• TauCeti.Manifold.variationField_chartVariation: its variation field.

References

• M. P. do Carmo, Riemannian Geometry, Birkhäuser, 1992, Ch. 9, §2, proof of Proposition 2.5 (variations along a field f V supported near a parameter).

noncomputable def TauCeti.Manifold.chartVariation {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) (x₀ : M) (J : Set ℝ) (φ : ℝ → ℝ) (e : E) (s t : ℝ) : M

The variation of γ which, at the parameters of J, pushes γ t in the direction of the coordinate vector e of the extended chart at x₀, with profile φ: (s, t) ↦ ψ⁻¹ (ψ (γ t) + (s φ(t)) • e) for ψ = extChartAt I x₀. Outside J it is γ.

theorem TauCeti.Manifold.chartVariation_of_mem {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} {x₀ : M} {J : Set ℝ} {φ : ℝ → ℝ} {e : E} {t : ℝ} (ht : t ∈ J) (s : ℝ) : chartVariation I γ x₀ J φ e s t = ↑(extChartAt I x₀).symm (↑(extChartAt I x₀) (γ t) + (s * φ t) • e)

At a parameter of J, the chart variation is given by the chart formula.

@[simp]

theorem TauCeti.Manifold.chartVariation_of_notMem {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} {x₀ : M} {J : Set ℝ} {φ : ℝ → ℝ} {e : E} {t : ℝ} (ht : t ∉ J) (s : ℝ) : chartVariation I γ x₀ J φ e s t = γ t

Outside J, the chart variation is γ.

theorem TauCeti.Manifold.chartVariation_of_mul_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] {γ : ℝ → M} {x₀ : M} {J : Set ℝ} {φ : ℝ → ℝ} {e : E} (hJ : ∀ t ∈ J, γ t ∈ (extChartAt I x₀).source) {s t : ℝ} (h : s * φ t = 0) : chartVariation I γ x₀ J φ e s t = γ t

Where the displacement s φ(t) vanishes, the chart variation is γ.

theorem TauCeti.Manifold.chartVariation_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] {γ : ℝ → M} {x₀ : M} {J : Set ℝ} {φ : ℝ → ℝ} {e : E} (hJ : ∀ t ∈ J, γ t ∈ (extChartAt I x₀).source) : chartVariation I γ x₀ J φ e 0 = γ

The central curve of the chart variation is γ.

theorem TauCeti.Manifold.contMDiffAt_chartVariation {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 : ℕ∞} {γ : ℝ → M} {x₀ : M} {J : Set ℝ} {φ : ℝ → ℝ} {e : E} [I.Boundaryless] [IsManifold I (↑n) M] (hJo : IsOpen J) (hJ : ∀ t ∈ J, γ t ∈ (extChartAt I x₀).source) (hφ : ContDiff ℝ (↑n) φ) (hφJ : tsupport φ ⊆ J) {s t : ℝ} (hγ : ContMDiffAt (modelWithCornersSelf ℝ ℝ) I (↑n) γ t) (hT : t ∈ J → ↑(extChartAt I x₀) (γ t) + (s * φ t) • e ∈ (extChartAt I x₀).target) : ContMDiffAt (modelWithCornersSelf ℝ (ℝ × ℝ)) I (↑n) (fun (z : ℝ × ℝ) => chartVariation I γ x₀ J φ e z.1 z.2) (s, t)

On a C^n manifold without boundary, the chart variation of a curve which is C^n at t, for a C^n profile supported in the open set J, is C^n at (s, t) provided that, if t ∈ J, the displaced point ψ (γ t) + (s φ(t)) • e lies in the chart target.

theorem TauCeti.Manifold.variationField_chartVariation {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} {x₀ : M} {J : Set ℝ} {φ : ℝ → ℝ} {e : E} [I.Boundaryless] [IsManifold I 1 M] (hJ : ∀ t ∈ J, γ t ∈ (extChartAt I x₀).source) {t : ℝ} (htJ : t ∈ J) : variationField I (chartVariation I γ x₀ J φ e) t = φ t • (Bundle.Trivialization.symmL ℝ (trivializationAt E (TangentSpace I) x₀) (γ t)) e

At a parameter of J, the variation field of the chart variation is φ t times the tangent vector at γ t with coordinates e in the tangent-bundle trivialization at x₀.