The path traced by a function on an open interval

A curve is often produced not as a Path but as a function g : ℝ → X defined on an open interval Ioo a b, continuous there, and converging at each of the two ends. This file turns such a function into an honest Path between its two limits, TauCeti.Path.ofContinuousOnIoo, and records what its values are on the interior of the unit interval and what its range is.

The construction is the extension TauCeti.extendIoo a b u v g of g across the two ends of the interval by the prescribed values u and v, composed with the affine reparametrisation AffineMap.lineMap a b : [0, 1] → [a, b]. Because those two values are given rather than recovered as limits, the continuity of the extension on Icc a b (TauCeti.continuousOn_Icc_extendIoo) needs no separation assumption on X, unlike Mathlib's continuousOn_Icc_extendFrom_Ioo for extendFrom, which must locate the limits and so asks for a regular codomain, and eq_lim_at_left_extendFrom_Ioo, which asks for a Hausdorff one. Nothing else is needed: the two endpoint limits are exactly the data that a Path between them requires.

The range is closure (g '' Ioo a b) rather than g '' Ioo a b: the path traverses the closed interval, and the image of a compact set under a map continuous on it is the closure of the image of the dense open part. So the closure of a curve given on an open interval is automatically path-connected, with the curve itself as the interior of the traversal — which is what makes this construction useful, since the endpoints are in general not values of g.

Simplicity

Whether the path is simple is not a matter of the extension but of g and of the endpoints, and the one step of that argument which is not a plain composition is recorded here, in the reparametrisation-only form and with no topology on X at all: TauCeti.eq_or_eq_endpoints_of_notMem_of_forall_mem_Ioo says that if a curve on the unit interval is injective on the interior, and that interior stays inside a set to which neither endpoint value belongs, then the only repetition left is between the two endpoints. That is the statement "the path is a simple arc, except that it may be a loop".

It is stated for a bare function unitInterval → X, with no hypothesis relating it to g or to the extension, rather than for TauCeti.Path.ofContinuousOnIoo itself: a consumer typically receives its path from an existential and knows only a parametrisation formula for it, which it uses to establish the membership and injectivity hypotheses; a Path specializes through its coercion. Injectivity on the interior is likewise left to the call site, being the injectivity of g composed with that of AffineMap.lineMap a b.

Main declarations

• TauCeti.extendIoo — a function on Ioo a b, extended across both ends by prescribed values, with TauCeti.extendIoo_apply_of_mem_Ioo, TauCeti.extendIoo_apply_of_le_left and TauCeti.extendIoo_apply_of_left_lt_of_right_le computing it at every point, and TauCeti.continuousOn_Icc_extendIoo, its continuity on Icc a b.
• TauCeti.Path.ofContinuousOnIoo — the path traced by a function continuous on Ioo a b with a limit at each end, from the limit at a to the limit at b.
• TauCeti.Path.ofContinuousOnIoo_apply and TauCeti.Path.ofContinuousOnIoo_apply_of_mem_Ioo — its values, in general and on the interior.
• TauCeti.Path.range_ofContinuousOnIoo — its range is closure (g '' Ioo a b).
• TauCeti.eq_or_eq_endpoints_of_notMem_of_forall_mem_Ioo — the simplicity lemma above; it runs on Mathlib's trichotomy Set.eq_endpoints_or_mem_Ioo_of_mem_Icc, read on the unit interval.

Generality

The extension and its continuity are stated over an arbitrary linearly ordered domain with an order-closed topology; only the path is real, AffineMap.lineMap and unitInterval being so. The path and its values ask nothing of X beyond a topology; only the range computation is Hausdorff, the image of a compact set having to be closed there. The simplicity lemma assumes nothing about X at all.

theorem TauCeti.eq_or_eq_endpoints_of_notMem_of_forall_mem_Ioo {X : Type u_1} {γ : ↑unitInterval → X} {S : Set X} (hzero : γ 0 ∉ S) (hone : γ 1 ∉ S) (hmem : ∀ t ∈ Set.Ioo 0 1, γ t ∈ S) (hinj : Set.InjOn γ (Set.Ioo 0 1)) ⦃x y : ↑unitInterval⦄ (hxy : γ x = γ y) : x = y ∨ x = 0 ∧ y = 1 ∨ x = 1 ∧ y = 0

A path repeats only at its endpoints when its interior avoids both endpoint values. If γ maps the open interval into S, neither endpoint value lies in S, and γ is injective on the open interval, then any repeated value is a common value of the two endpoints.

Purely a statement about function values: neither γ nor S carries any topology, and a Path specializes automatically through its coercion. The frontier/open-set form is derived at the call site.

noncomputable def TauCeti.extendIoo {X : Type u_1} {α : Type u_2} [LinearOrder α] (a b : α) (u v : X) (g : α → X) : α → X

A function on an open interval, extended across both of its ends by prescribed values. TauCeti.extendIoo a b u v g agrees with g on Ioo a b and takes the value u on Iic a; when a < b it takes the value v on Ici b, so that in particular it is u at a and v at b. The two outer branches run over the whole of Iic a and Ici b, rather than over the endpoints alone, so that the definition computes everywhere and carries no side condition. The nondegeneracy a < b is not part of the definition, and is needed for the right-hand branch only: if instead b ≤ a, the interval is empty and the extension is u on Iic a and v on Ioi a, so that b itself is sent to u. The value is therefore computed at every point of α, degenerate intervals included, by TauCeti.extendIoo_apply_of_mem_Ioo, TauCeti.extendIoo_apply_of_le_left and TauCeti.extendIoo_apply_of_left_lt_of_right_le, whose hypotheses are exactly the three branch conditions.

Mathlib's extendFrom instead recovers the end values as limits, which is why its continuity theorem continuousOn_Icc_extendFrom_Ioo asks for a regular codomain and its identification theorem eq_lim_at_left_extendFrom_Ioo for a Hausdorff one. Here the end values are given, and TauCeti.continuousOn_Icc_extendIoo needs neither.

Equations

• TauCeti.extendIoo a b u v g x = if x ≤ a then u else if b ≤ x then v else g x

@[simp]

theorem TauCeti.extendIoo_apply_of_mem_Ioo {X : Type u_1} {α : Type u_2} [LinearOrder α] {a b x : α} {u v : X} {g : α → X} (hx : x ∈ Set.Ioo a b) : extendIoo a b u v g x = g x

Inside the open interval the extension is the function itself.

@[simp]

theorem TauCeti.extendIoo_apply_of_le_left {X : Type u_1} {α : Type u_2} [LinearOrder α] {a b x : α} {u v : X} {g : α → X} (hx : x ≤ a) : extendIoo a b u v g x = u

At and below the left end the extension takes the prescribed value u.

@[simp]

theorem TauCeti.extendIoo_apply_of_left_lt_of_right_le {X : Type u_1} {α : Type u_2} [LinearOrder α] {a b x : α} {u v : X} {g : α → X} (hax : a < x) (hx : b ≤ x) : extendIoo a b u v g x = v

Above the left end and at or above the right end the extension takes the prescribed value v. These are exactly the conditions of the second branch, so together with TauCeti.extendIoo_apply_of_mem_Ioo and TauCeti.extendIoo_apply_of_le_left this computes the extension at every point, degenerate intervals included.

theorem TauCeti.continuousOn_Icc_extendIoo {X : Type u_1} {α : Type u_2} [LinearOrder α] {a b : α} {u v : X} {g : α → X} [TopologicalSpace α] [OrderClosedTopology α] [TopologicalSpace X] (hab : a < b) (hg : ContinuousOn g (Set.Ioo a b)) (hu : Filter.Tendsto g (nhdsWithin a (Set.Ioi a)) (nhds u)) (hv : Filter.Tendsto g (nhdsWithin b (Set.Iio b)) (nhds v)) : ContinuousOn (extendIoo a b u v g) (Set.Icc a b)

A function continuous on an open interval and converging at both ends extends continuously to the closed interval. The extension is TauCeti.extendIoo by the two limits; being handed them, the proof glues at the two ends and asks nothing of X beyond a topology.

noncomputable def TauCeti.Path.ofContinuousOnIoo {X : Type u_1} [TopologicalSpace X] {a b : ℝ} {u v : X} {g : ℝ → X} (hab : a < b) (hg : ContinuousOn g (Set.Ioo a b)) (hu : Filter.Tendsto g (nhdsWithin a (Set.Ioi a)) (nhds u)) (hv : Filter.Tendsto g (nhdsWithin b (Set.Iio b)) (nhds v)) : Path u v

The path traced by a function on an open interval. If g is continuous on Ioo a b, tends to u at a from the right and to v at b from the left, then g traverses a path from u to v: the extension TauCeti.extendIoo a b u v g of g across the two ends, read along the affine parametrisation AffineMap.lineMap a b of Icc a b by the unit interval.

Its values on the interior of the unit interval are those of g (TauCeti.Path.ofContinuousOnIoo_apply_of_mem_Ioo) and its range is closure (g '' Ioo a b) (TauCeti.Path.range_ofContinuousOnIoo); the endpoints u and v need not themselves be values of g. Compute with it through TauCeti.Path.ofContinuousOnIoo_apply rather than through the definition.

Equations

• TauCeti.Path.ofContinuousOnIoo hab hg hu hv = { toFun := fun (t : ↑unitInterval) => TauCeti.extendIoo a b u v g ((AffineMap.lineMap a b) ↑t), continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }

theorem TauCeti.Path.ofContinuousOnIoo_apply {X : Type u_1} [TopologicalSpace X] {a b : ℝ} {u v : X} {g : ℝ → X} (hab : a < b) (hg : ContinuousOn g (Set.Ioo a b)) (hu : Filter.Tendsto g (nhdsWithin a (Set.Ioi a)) (nhds u)) (hv : Filter.Tendsto g (nhdsWithin b (Set.Iio b)) (nhds v)) (t : ↑unitInterval) : (ofContinuousOnIoo hab hg hu hv) t = extendIoo a b u v g ((AffineMap.lineMap a b) ↑t)

The path traced by g is the extension of g across the two ends of Ioo a b, read along the affine parametrisation of Icc a b by the unit interval.

@[simp]

theorem TauCeti.Path.ofContinuousOnIoo_apply_of_mem_Ioo {X : Type u_1} [TopologicalSpace X] {a b : ℝ} {u v : X} {g : ℝ → X} (hab : a < b) (hg : ContinuousOn g (Set.Ioo a b)) (hu : Filter.Tendsto g (nhdsWithin a (Set.Ioi a)) (nhds u)) (hv : Filter.Tendsto g (nhdsWithin b (Set.Iio b)) (nhds v)) {t : ↑unitInterval} (ht : t ∈ Set.Ioo 0 1) : (ofContinuousOnIoo hab hg hu hv) t = g ((AffineMap.lineMap a b) ↑t)

On the interior of the unit interval the path traced by g is g itself, along the affine parametrisation. The endpoints are excluded because there the values of g are unconstrained: they need not be the limits u and v, which is what makes the construction more than a reparametrisation.

theorem TauCeti.Path.range_ofContinuousOnIoo {X : Type u_1} [TopologicalSpace X] {a b : ℝ} {u v : X} {g : ℝ → X} [T2Space X] (hab : a < b) (hg : ContinuousOn g (Set.Ioo a b)) (hu : Filter.Tendsto g (nhdsWithin a (Set.Ioi a)) (nhds u)) (hv : Filter.Tendsto g (nhdsWithin b (Set.Iio b)) (nhds v)) : Set.range ⇑(ofContinuousOnIoo hab hg hu hv) = closure (g '' Set.Ioo a b)

The range of the path traced by g is the closure of the curve. The path traverses the closed interval Icc a b, which is the closure of Ioo a b and compact, so its image under a map continuous there is the closure of the image of Ioo a b. In particular the closure of a curve defined on an open interval and converging at both ends is path-connected.