Smooth time maps into the unit interval

The reflection t ↦ 1 - t and the multiplication (s, t) ↦ s t are smooth for the manifold-with-boundary structure of the unit interval. The smooth transition function also gives smooth interval-valued maps. These support reversal, rescaling and stationary-time concatenation of smooth isotopies.

The constructions reuse Mathlib’s interval immersion and Real.smoothTransition. The preferred interval charts also expose their actual affine coordinate formulas and the within-range derivatives of the inclusion composed with their inverses. The derivative of the inclusion is invertible at every point, including both endpoints.

Both preferred charts send their endpoints to 0 (extChartAt_Icc_bot, extChartAt_Icc_top).

theorem unitInterval.contMDiff_symm {n : WithTop ℕ∞} : ContMDiff (modelWithCornersEuclideanHalfSpace 1) (modelWithCornersEuclideanHalfSpace 1) n symm

Time reversal is smooth, including at both endpoints of the unit interval.

instance unitInterval.instContMDiffMulRealEuclideanHalfSpaceOfNatNatEuclideanSpaceFinModelWithCornersEuclideanHalfSpaceTopWithTopENatElem_tauCeti : ContMDiffMul (modelWithCornersEuclideanHalfSpace 1) ⊤ ↑unitInterval

Multiplication (s, t) ↦ s t of the unit interval is analytic, including at the boundary, so it is C^n for every n (contMDiff_mul).

theorem ContMDiff.smoothTransition {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 → ℝ} (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) n f) (hn : n ≤ ↑⊤) : ContMDiff I (modelWithCornersEuclideanHalfSpace 1) n fun (x : M) => ⟨(f x).smoothTransition, ⋯⟩

Applying the smooth transition function gives a smooth map into the unit interval. This applies to finite regularity and C^∞, without asserting analyticity.

theorem TauCeti.extChartAt_Icc_apply {a b : ℝ} [hab : Fact (a < b)] (α x : ↑(Set.Icc a b)) : ↑(extChartAt (modelWithCornersEuclideanHalfSpace 1) α) x = if ↑α < b then WithLp.toLp 2 fun (x_1 : Fin 1) => ↑x - a else WithLp.toLp 2 fun (x_1 : Fin 1) => b - ↑x

Mathlib's actual preferred interval chart is translation on the left and reflection on the right. This formula holds for every input, independently of chart-source membership.

theorem TauCeti.extChartAt_Icc_target {a b : ℝ} [hab : Fact (a < b)] (α : ↑(Set.Icc a b)) : (extChartAt (modelWithCornersEuclideanHalfSpace 1) α).target = (fun (z : EuclideanSpace ℝ (Fin 1)) => z.ofLp 0) ⁻¹' Set.Ico 0 (b - a)

Both preferred interval charts have the actual half-open coordinate target [0,b-a).

theorem TauCeti.subtypeVal_extChartAt_Icc_symm {a b : ℝ} [hab : Fact (a < b)] (α : ↑(Set.Icc a b)) {z : EuclideanSpace ℝ (Fin 1)} (hz : z ∈ (extChartAt (modelWithCornersEuclideanHalfSpace 1) α).target) : ↑(↑(extChartAt (modelWithCornersEuclideanHalfSpace 1) α).symm z) = if ↑α < b then z.ofLp 0 + a else b - z.ofLp 0

On the actual coordinate target, the inverse interval chart composed with inclusion is affine; the model retraction and interval clamps do not alter these values.

theorem TauCeti.hasFDerivWithinAt_subtypeVal_extChartAt_Icc_symm {a b : ℝ} [hab : Fact (a < b)] (α : ↑(Set.Icc a b)) {z : EuclideanSpace ℝ (Fin 1)} (hz : z ∈ (extChartAt (modelWithCornersEuclideanHalfSpace 1) α).target) : HasFDerivWithinAt (fun (w : EuclideanSpace ℝ (Fin 1)) => ↑(↑(extChartAt (modelWithCornersEuclideanHalfSpace 1) α).symm w)) ((if ↑α < b then 1 else -1) • EuclideanSpace.proj 0) (Set.range ↑(modelWithCornersEuclideanHalfSpace 1)) z

The actual inverse interval chart has derivative +eval₀ in the left chart and -eval₀ in the right chart, including derivatives within the half-line at its endpoint.

theorem TauCeti.mfderiv_subtypeVal_Icc {a b : ℝ} [hab : Fact (a < b)] (x : ↑(Set.Icc a b)) : mfderiv% Subtype.val x = (if ↑x < b then 1 else -1) • EuclideanSpace.proj 0

The interval inclusion has its actual signed own-chart derivative. At the right endpoint the inward half-line coordinate points in the negative real direction.

theorem TauCeti.interior_Icc_subset_extChartAt_bot_source {a b : ℝ} [hab : Fact (a < b)] : ModelWithCorners.interior ↑(Set.Icc a b) ⊆ (extChartAt (modelWithCornersEuclideanHalfSpace 1) ⊥).source

Every intrinsic interior point of the interval belongs to its bottom preferred chart.

theorem TauCeti.tangentCoordChange_Icc {a b : ℝ} [hab : Fact (a < b)] (α β x : ↑(Set.Icc a b)) (hx : x ∈ (extChartAt (modelWithCornersEuclideanHalfSpace 1) α).source) : tangentCoordChange (modelWithCornersEuclideanHalfSpace 1) α β x = ((if ↑β < b then 1 else -1) * if ↑α < b then 1 else -1) • ContinuousLinearMap.id ℝ (EuclideanSpace ℝ (Fin 1))

The preferred interval transition derivative is the product of the two chart signs.

noncomputable def TauCeti.subtypeValIccTangentEquiv {a b : ℝ} (x : ↑(Set.Icc a b)) : EuclideanSpace ℝ (Fin 1) ≃L[ℝ] ℝ

The derivative of interval inclusion, on its canonical tangent model and identified with the real target model, as an invertible continuous linear map. Its own-chart sign changes at the right endpoint.

@[simp]

theorem TauCeti.subtypeValIccTangentEquiv_apply {a b : ℝ} (x : ↑(Set.Icc a b)) (v : EuclideanSpace ℝ (Fin 1)) : (subtypeValIccTangentEquiv x) v = (if ↑x < b then 1 else -1) * (EuclideanSpace.proj 0) v

The interval inclusion tangent equivalence is the signed coordinate projection.

@[simp]

theorem TauCeti.subtypeValIccTangentEquiv_symm_apply {a b : ℝ} (x : ↑(Set.Icc a b)) (r : ℝ) (i : Fin 1) : ((subtypeValIccTangentEquiv x).symm r).ofLp i = (if ↑x < b then 1 else -1) * r

The inverse interval tangent equivalence multiplies the real coordinate by the chart sign.

theorem TauCeti.subtypeValIccTangentEquiv_toContinuousLinearMap {a b : ℝ} [hab : Fact (a < b)] (x : ↑(Set.Icc a b)) : ↑(subtypeValIccTangentEquiv x) = ↑(NormedSpace.fromTangentSpace ↑x) ∘SL mfderiv% Subtype.val x

The tangent equivalence is the actual inclusion derivative, with the canonical real model tangent identification on its target.

theorem TauCeti.isInvertible_mfderiv_subtypeVal_Icc {a b : ℝ} [hab : Fact (a < b)] (x : ↑(Set.Icc a b)) : (mfderiv% Subtype.val x).IsInvertible

The derivative of the interval inclusion is invertible at every point, including both endpoints.

theorem TauCeti.mfderiv_interval_affine_apply {a b : ℝ} [Fact (a < b)] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] (z : F) (L : ℝ →L[ℝ] F) (x : ↑(Set.Icc a b)) (w : TangentSpace (modelWithCornersEuclideanHalfSpace 1) x) : (NormedSpace.fromTangentSpace (z + L ↑x)) (((mfderiv% fun (t : ↑(Set.Icc a b)) => z + L ↑t) x) w) = L ((subtypeValIccTangentEquiv x) w)

The derivative of an affine map from the interval to any real normed space is its linear part applied to the actual interval inclusion derivative, including at both endpoints.

theorem TauCeti.extChartAt_Icc_bot {a b : ℝ} [hab : Fact (a < b)] : ↑(extChartAt (modelWithCornersEuclideanHalfSpace 1) ⊥) ⊥ = 0

The preferred chart of [a, b] at its bottom endpoint sends it to 0.

theorem TauCeti.extChartAt_Icc_top {a b : ℝ} [hab : Fact (a < b)] : ↑(extChartAt (modelWithCornersEuclideanHalfSpace 1) ⊤) ⊤ = 0

The preferred chart of [a, b] at its top endpoint sends it to 0.