Manifold structure on real intervals

The manifold structure on real intervals is defined in Mathlib.Geometry.Manifold.Instances.Real. We relate it to the manifold structure on the real line, by showing that the inclusion (contMDiff_subtype_coe_Icc) and projection (contMDiffOn_projIcc) are smooth, and showing that a function defined on the interval is smooth iff its composition with the projection is smooth on the interval in ℝ (see contMDiffOn_comp_projIcc_iff and friends).

We also define 1 : TangentSpace (𝓡∂ 1) z, and relate it to 1 in the real line.

TODO

This file can be thoroughly rewritten once mathlib has a good theory of smooth immersions and embeddings. Once this is done,

• the inclusion Icc x y → ℝ is a smooth embedding, and in particular smooth
• deduce the dual result: a function f : M → Icc x y is smooth iff its composition with the inclusion into ℝ is smooth
• prove the projection ℝ → Icc x y is a smooth submersion, hence smooth
• use this to simplify the proof that f : Icc x y → M is smooth iff the composition ℝ → M with the projection ℝ → Icc x y is

instance instOneTangentSpaceRealModelWithCornersSelf (x : ℝ) : One (TangentSpace (modelWithCornersSelf ℝ ℝ) x)

Equations

• instOneTangentSpaceRealModelWithCornersSelf x = { one := 1 }

theorem oneTangentSpaceIcc_def {x y : ℝ} [h : Fact (x < y)] (z : ↑(Set.Icc x y)) : oneTangentSpaceIcc z = (mfderivWithin (modelWithCornersSelf ℝ ℝ) (modelWithCornersEuclideanHalfSpace 1) (Set.projIcc x y ⋯) (Set.Icc x y) ↑z) 1

@[irreducible]

def oneTangentSpaceIcc {x y : ℝ} [h : Fact (x < y)] (z : ↑(Set.Icc x y)) : TangentSpace (modelWithCornersEuclideanHalfSpace 1) z

Unit vector in the tangent space to a segment, as the image of the unit vector in the real line under the canonical projection. It is also mapped to the unit vector in the real line through the canonical injection, see mfderiv_subtype_coe_Icc_one.

Note that one can not abuse defeqs for this definition: this is not the same as the vector fun _ ↦ 1 in EuclideanSpace ℝ (Fin 1) through defeqs, as one of the charts of Icc x y is orientation-reversing.

Equations

• oneTangentSpaceIcc z = (mfderivWithin (modelWithCornersSelf ℝ ℝ) (modelWithCornersEuclideanHalfSpace 1) (Set.projIcc x y ⋯) (Set.Icc x y) ↑z) 1

instance instOneTangentSpaceRealEuclideanSpaceFinOfNatNatEuclideanHalfSpaceModelWithCornersEuclideanHalfSpaceElemIcc {x y : ℝ} [h : Fact (x < y)] (z : ↑(Set.Icc x y)) : One (TangentSpace (modelWithCornersEuclideanHalfSpace 1) z)

Equations

• instOneTangentSpaceRealEuclideanSpaceFinOfNatNatEuclideanHalfSpaceModelWithCornersEuclideanHalfSpaceElemIcc z = { one := oneTangentSpaceIcc z }

theorem contMDiff_subtype_coe_Icc {x y : ℝ} [h : Fact (x < y)] {n : WithTop ℕ∞} : ContMDiff (modelWithCornersEuclideanHalfSpace 1) (modelWithCornersSelf ℝ ℝ) n fun (z : ↑(Set.Icc x y)) => ↑z

The inclusion map from of a closed segment to ℝ is smooth in the manifold sense.

theorem contMDiffOn_projIcc {x y : ℝ} [h : Fact (x < y)] {n : WithTop ℕ∞} : ContMDiffOn (modelWithCornersSelf ℝ ℝ) (modelWithCornersEuclideanHalfSpace 1) n (Set.projIcc x y ⋯) (Set.Icc x y)

The projection from ℝ to a closed segment is smooth on the segment, in the manifold sense.

theorem contMDiffOn_comp_projIcc_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] {x y : ℝ} [h : Fact (x < y)] {n : WithTop ℕ∞} {f : ↑(Set.Icc x y) → M} : ContMDiffOn (modelWithCornersSelf ℝ ℝ) I n (f ∘ Set.projIcc x y ⋯) (Set.Icc x y) ↔ ContMDiff (modelWithCornersEuclideanHalfSpace 1) I n f

theorem contMDiffWithinAt_comp_projIcc_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] {x y : ℝ} [h : Fact (x < y)] {n : WithTop ℕ∞} {f : ↑(Set.Icc x y) → M} {w : ↑(Set.Icc x y)} : ContMDiffWithinAt (modelWithCornersSelf ℝ ℝ) I n (f ∘ Set.projIcc x y ⋯) (Set.Icc x y) ↑w ↔ ContMDiffAt (modelWithCornersEuclideanHalfSpace 1) I n f w

theorem mdifferentiableWithinAt_comp_projIcc_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] {x y : ℝ} [h : Fact (x < y)] {f : ↑(Set.Icc x y) → M} {w : ↑(Set.Icc x y)} : MDifferentiableWithinAt (modelWithCornersSelf ℝ ℝ) I (f ∘ Set.projIcc x y ⋯) (Set.Icc x y) ↑w ↔ MDifferentiableAt (modelWithCornersEuclideanHalfSpace 1) I f w

theorem mfderivWithin_projIcc_one {x y : ℝ} [h : Fact (x < y)] {z : ℝ} (hz : z ∈ Set.Icc x y) : (mfderivWithin (modelWithCornersSelf ℝ ℝ) (modelWithCornersEuclideanHalfSpace 1) (Set.projIcc x y ⋯) (Set.Icc x y) z) 1 = 1

theorem mfderivWithin_comp_projIcc_one {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] {x y : ℝ} [h : Fact (x < y)] {f : ↑(Set.Icc x y) → M} {w : ↑(Set.Icc x y)} : (mfderivWithin (modelWithCornersSelf ℝ ℝ) I (f ∘ Set.projIcc x y ⋯) (Set.Icc x y) ↑w) 1 = (mfderiv (modelWithCornersEuclideanHalfSpace 1) I f w) 1

theorem mfderiv_subtype_coe_Icc_one {x y : ℝ} [h : Fact (x < y)] (z : ↑(Set.Icc x y)) : (mfderiv (modelWithCornersEuclideanHalfSpace 1) (modelWithCornersSelf ℝ ℝ) Subtype.val z) 1 = 1