Piecewise smooth paths in a manifold

This file defines piecewise C^n regularity for a path on a compact real interval using a finite strict partition. The predicate retains the partition only existentially. Thus two proofs using different partitions are proofs of the same property of the underlying path, rather than distinct bundled paths carrying irrelevant partition data.

Main definitions

• TauCeti.Manifold.IsPiecewiseContMDiffOn: a path is C^n on the pieces of some finite strict partition of [a, b].

Main results

• TauCeti.Manifold.IsPiecewiseContMDiffOn.exists_partition: extract a witnessing strict partition and the piecewise regularity facts.
• TauCeti.Manifold.IsPiecewiseContMDiffOn.of_partition: construct piecewise regularity from a strict partition and regularity on each piece.
• TauCeti.Manifold.IsPiecewiseContMDiffOn.continuousOn: piecewise C^n regularity implies continuity on the whole interval.
• TauCeti.Manifold.IsPiecewiseContMDiffOn.trans_contMDiffOn and TauCeti.Manifold.IsPiecewiseContMDiffOn.mono: appending a C^n piece and restricting to a nondegenerate subinterval preserve piecewise C^n regularity.

This is a metric-independent finite-partition regularity API for curves in a manifold: it only involves the differentiable structure, so that Riemannian length and distance comparisons can be built on top of it by integrating along the pieces. The explicit-partition subinterval induction follows the pattern of the Apache-2.0 frenzymath/Poincare-Conjecture formalization, revision 24f32e4d600878bfaac6bc2f2f9324175571c321, as used in TauCeti/Geometry/Manifold/Riemannian/EDistComparison.lean.

References

• M. P. do Carmo, Riemannian Geometry, Chapter 1, Definition 2.9 and Chapter 7, Section 2.

def TauCeti.Manifold.IsPiecewiseContMDiffOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {M : Type u} [TopologicalSpace M] [ChartedSpace H M] (I : ModelWithCorners ℝ E H) (n : WithTop ℕ∞) (γ : ℝ → M) (a b : ℝ) : Prop

A path is piecewise C^n on [a, b] if there is a nonempty finite strict partition from a to b such that the path is C^n on every closed piece. The partition has k + 1 pieces and k + 2 vertices, so the definition includes the one-piece case but excludes a vacuous zero-piece witness.

The partition is existential data because it witnesses a property of γ; it is not part of the identity of a path. In particular, refining a partition does not create a different object.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.Manifold.IsPiecewiseContMDiffOn.exists_partition {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} {γ : ℝ → M} {a b : ℝ} (h : IsPiecewiseContMDiffOn I n γ a b) : ∃ (k : ℕ) (τ : Fin (k + 2) → ℝ), τ 0 = a ∧ τ (Fin.last (k + 1)) = b ∧ (∀ (i : Fin (k + 1)), τ i.castSucc < τ i.succ) ∧ ∀ (i : Fin (k + 1)), ContMDiffOn (modelWithCornersSelf ℝ ℝ) I n γ (Set.Icc (τ i.castSucc) (τ i.succ))

Extract a strict partition witnessing piecewise C^n regularity, together with the C^n restriction on each closed piece.

theorem TauCeti.Manifold.IsPiecewiseContMDiffOn.of_partition {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} {γ : ℝ → M} {a b : ℝ} {k : ℕ} (τ : Fin (k + 2) → ℝ) (hτa : τ 0 = a) (hτb : τ (Fin.last (k + 1)) = b) (hτ : ∀ (i : Fin (k + 1)), τ i.castSucc < τ i.succ) (hγ : ∀ (i : Fin (k + 1)), ContMDiffOn (modelWithCornersSelf ℝ ℝ) I n γ (Set.Icc (τ i.castSucc) (τ i.succ))) : IsPiecewiseContMDiffOn I n γ a b

A strict finite partition on whose pieces a path is C^n witnesses piecewise C^n regularity.

theorem TauCeti.Manifold.IsPiecewiseContMDiffOn.lt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} {γ : ℝ → M} {a b : ℝ} (h : IsPiecewiseContMDiffOn I n γ a b) : a < b

The endpoints of a piecewise smooth path are strictly ordered.

theorem TauCeti.Manifold.IsPiecewiseContMDiffOn.of_contMDiffOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} {γ : ℝ → M} {a b : ℝ} (hab : a < b) (hγ : ContMDiffOn (modelWithCornersSelf ℝ ℝ) I n γ (Set.Icc a b)) : IsPiecewiseContMDiffOn I n γ a b

A C^n path on a nondegenerate interval is piecewise C^n, witnessed by the partition consisting only of its two endpoints.

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

Restricting the requested differentiability order preserves piecewise smoothness.

theorem TauCeti.Manifold.IsPiecewiseContMDiffOn.continuousOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} {γ : ℝ → M} {a b : ℝ} (h : IsPiecewiseContMDiffOn I n γ a b) : ContinuousOn γ (Set.Icc a b)

Piecewise C^n regularity implies continuity on the whole interval.

theorem TauCeti.Manifold.IsPiecewiseContMDiffOn.trans_contMDiffOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} {γ : ℝ → M} {a b : ℝ} (h : IsPiecewiseContMDiffOn I n γ a b) {c : ℝ} (hbc : b < c) (hγ : ContMDiffOn (modelWithCornersSelf ℝ ℝ) I n γ (Set.Icc b c)) : IsPiecewiseContMDiffOn I n γ a c

Appending a C^n piece to a piecewise C^n path gives a piecewise C^n path: the new vertex is added at the end of a witnessing partition.

theorem TauCeti.Manifold.IsPiecewiseContMDiffOn.mono {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} {γ : ℝ → M} {a b : ℝ} (h : IsPiecewiseContMDiffOn I n γ a b) {s t : ℝ} (has : a ≤ s) (hst : s < t) (htb : t ≤ b) : IsPiecewiseContMDiffOn I n γ s t

A piecewise C^n path is piecewise C^n on every nondegenerate subinterval of its parameter interval.