Closures of bands and band interpolation maps

A band over a set s ⊆ X is the region between two real functions on s: Mathlib's open regionBetween φ φ' s, and its closed counterpart TauCeti.closedRegionBetween φ φ' s. Bands and graphs over the simplices of a base triangulation are the cells of the prismatic decomposition in Łojasiewicz's triangulation of semianalytic sets. This file develops the elementary endpoint calculus which glues the cell maps of that construction.

• TauCeti.closure_regionBetween: if φ < φ' on s and both are continuous on closure s, then the closure of the open band over s is the closed band over closure s. TauCeti.closure_regionBetween_of_closure_graphOn_eq states this, following Łojasiewicz, for endpoint functions whose graph closures are bounded single-valued functions on closure s.
• TauCeti.regionBetweenMap g φ φ' ψ ψ': over a base map g, the map interpolating affinely between the fibres [φ x, φ' x] and [ψ (g x), ψ' (g x)], lower endpoint to lower endpoint. A collapsed fibre φ x = φ' x is sent to (g x, ψ (g x)), so for ordered endpoints a source fibre is mapped onto its target fibre when it is nondegenerate, or when both fibres collapse.
• Graph and restriction compatibility: the band map restricts to the graph maps of its endpoints (TauCeti.image_regionBetweenMap_graphOn_lower, TauCeti.image_regionBetweenMap_graphOn_upper) and depends only on the data over the points it is evaluated at (TauCeti.eqOn_regionBetweenMap). It maps closed bands to closed bands and open bands to open bands, and the band map of an inverse base map is its inverse (TauCeti.bijOn_regionBetweenMap, TauCeti.bijOn_regionBetweenMap_regionBetween).
• TauCeti.continuousOn_regionBetweenMap: the band map is continuous on the closed band whenever the base and endpoint maps are continuous and every collapsed source fibre lies over a collapsed target fibre.
• OpenPartialHomeomorph.regionBetween: when the base map is an open partial homeomorphism and the continuous endpoints are strictly ordered, interpolation is an open partial homeomorphism between the open bands. Its inverse uses the inverse base map with the endpoint pairs exchanged.

References

• S. Łojasiewicz, Triangulation of semi-analytic sets, Ann. Scuola Norm. Sup. Pisa (3) 18 (1964), 449–474, §2, Lemmas 11, 12 and 14.

def TauCeti.closedRegionBetween {α : Type u_1} (f g : α → ℝ) (s : Set α) : Set (α × ℝ)

The closed region between two real-valued functions on a set: the points (x, t) with x ∈ s and f x ≤ t ≤ g x. This is the closed counterpart of regionBetween f g s.

@[simp]

theorem TauCeti.mem_closedRegionBetween {α : Type u_1} {f g : α → ℝ} {s : Set α} {p : α × ℝ} : p ∈ closedRegionBetween f g s ↔ p.1 ∈ s ∧ p.2 ∈ Set.Icc (f p.1) (g p.1)

theorem TauCeti.regionBetween_subset_closedRegionBetween {α : Type u_1} (f g : α → ℝ) (s : Set α) : regionBetween f g s ⊆ closedRegionBetween f g s

@[simp]

theorem TauCeti.closedRegionBetween_self {α : Type u_1} (f : α → ℝ) (s : Set α) : closedRegionBetween f f s = Set.graphOn f s

The closed region between a function and itself is its graph.

@[simp]

theorem TauCeti.closedRegionBetween_const {α : Type u_1} (s : Set α) (y₁ y₂ : ℝ) : closedRegionBetween (Function.const α y₁) (Function.const α y₂) s = s ×ˢ Set.Icc y₁ y₂

The closed region between two constant functions over a set s is the prism s ×ˢ Icc y₁ y₂.

theorem TauCeti.regionBetween_congr {α : Type u_1} {f f' g g' : α → ℝ} {s : Set α} (hf : Set.EqOn f f' s) (hg : Set.EqOn g g' s) : regionBetween f g s = regionBetween f' g' s

The region between two functions only depends on their values on the base set.

theorem TauCeti.closedRegionBetween_congr {α : Type u_1} {f f' g g' : α → ℝ} {s : Set α} (hf : Set.EqOn f f' s) (hg : Set.EqOn g g' s) : closedRegionBetween f g s = closedRegionBetween f' g' s

The closed region between two functions only depends on their values on the base set.

theorem TauCeti.closedRegionBetween_eq_union {α : Type u_1} {f g : α → ℝ} {s : Set α} (h : ∀ x ∈ s, f x ≤ g x) : closedRegionBetween f g s = Set.graphOn f s ∪ regionBetween f g s ∪ Set.graphOn g s

The closed region between two ordered functions is the union of the open region and the two graphs.

theorem TauCeti.isClosed_closedRegionBetween {α : Type u_1} [TopologicalSpace α] {f g : α → ℝ} {s : Set α} (hs : IsClosed s) (hf : ContinuousOn f s) (hg : ContinuousOn g s) : IsClosed (closedRegionBetween f g s)

The closed region between two functions continuous on a closed set is closed.

theorem TauCeti.closure_regionBetween {α : Type u_1} [TopologicalSpace α] {f g : α → ℝ} {s : Set α} (hf : ContinuousOn f (closure s)) (hg : ContinuousOn g (closure s)) (hfg : ∀ x ∈ s, f x < g x) : closure (regionBetween f g s) = closedRegionBetween f g (closure s)

Łojasiewicz's band closure lemma, for endpoints continuous on the closure of the base: if f < g on s, then the closure of the open band between f and g over s is the closed band over closure s.

theorem TauCeti.closure_regionBetween_of_closure_graphOn_eq {α : Type u_1} [TopologicalSpace α] {f g F G : α → ℝ} {s : Set α} (hF : closure (Set.graphOn f s) = Set.graphOn F (closure s)) (hG : closure (Set.graphOn g s) = Set.graphOn G (closure s)) (hFb : Bornology.IsBounded (F '' closure s)) (hGb : Bornology.IsBounded (G '' closure s)) (hfg : ∀ x ∈ s, f x < g x) : closure (regionBetween f g s) = closedRegionBetween F G (closure s)

Łojasiewicz's band closure lemma: if f < g on s and the closures of the graphs of f and g over s are the graphs over closure s of bounded functions F and G, then the closure of the open band between f and g over s is the closed band between F and G over closure s.

noncomputable def TauCeti.regionBetweenMap {X : Type u_1} {Y : Type u_2} (g : X → Y) (φ φ' : X → ℝ) (ψ ψ' : Y → ℝ) (p : X × ℝ) : Y × ℝ

The band interpolation map over a base map g : X → Y, from the band between φ and φ' to the band between ψ and ψ'. It sends (x, t) to (g x, s) where s = ψ (g x) + (t - φ x) / (φ' x - φ x) * (ψ' (g x) - ψ (g x)). If φ x < φ' x and ψ (g x) ≤ ψ' (g x), it maps the fibre [φ x, φ' x] affinely onto [ψ (g x), ψ' (g x)]. When the source endpoints coincide, the quotient is 0 and the point is sent to (g x, ψ (g x)) (regionBetweenMap_of_eq), so a collapsed source fibre is mapped onto its target fibre only when that collapses too.

theorem TauCeti.regionBetweenMap_apply {X : Type u_1} {Y : Type u_2} (g : X → Y) (φ φ' : X → ℝ) (ψ ψ' : Y → ℝ) (x : X) (r : ℝ) : regionBetweenMap g φ φ' ψ ψ' (x, r) = (g x, ψ (g x) + (r - φ x) / (φ' x - φ x) * (ψ' (g x) - ψ (g x)))

@[simp]

theorem TauCeti.regionBetweenMap_fst {X : Type u_1} {Y : Type u_2} {g : X → Y} {φ φ' : X → ℝ} {ψ ψ' : Y → ℝ} (p : X × ℝ) : (regionBetweenMap g φ φ' ψ ψ' p).1 = g p.1

@[simp]

theorem TauCeti.regionBetweenMap_snd {X : Type u_1} {Y : Type u_2} {g : X → Y} {φ φ' : X → ℝ} {ψ ψ' : Y → ℝ} (p : X × ℝ) : (regionBetweenMap g φ φ' ψ ψ' p).2 = ψ (g p.1) + (p.2 - φ p.1) / (φ' p.1 - φ p.1) * (ψ' (g p.1) - ψ (g p.1))

The height coordinate of the band map is affine interpolation between the endpoints.

@[simp]

theorem TauCeti.regionBetweenMap_of_eq {X : Type u_1} {Y : Type u_2} {g : X → Y} {φ φ' : X → ℝ} {ψ ψ' : Y → ℝ} {x : X} (h : φ x = φ' x) (r : ℝ) : regionBetweenMap g φ φ' ψ ψ' (x, r) = (g x, ψ (g x))

Over a collapsed fibre φ x = φ' x, the band map is the graph map of the lower target endpoint.

@[simp]

theorem TauCeti.regionBetweenMap_lower {X : Type u_1} {Y : Type u_2} {g : X → Y} {φ φ' : X → ℝ} {ψ ψ' : Y → ℝ} (x : X) : regionBetweenMap g φ φ' ψ ψ' (x, φ x) = (g x, ψ (g x))

@[simp]

theorem TauCeti.regionBetweenMap_upper {X : Type u_1} {Y : Type u_2} {g : X → Y} {φ φ' : X → ℝ} {ψ ψ' : Y → ℝ} {x : X} (h : φ x = φ' x → ψ (g x) = ψ' (g x)) : regionBetweenMap g φ φ' ψ ψ' (x, φ' x) = (g x, ψ' (g x))

The band map sends the upper source endpoint to the upper target endpoint, provided a collapsed source fibre lies over a collapsed target fibre.

theorem TauCeti.image_regionBetweenMap_graphOn_lower {X : Type u_1} {Y : Type u_2} (g : X → Y) (φ φ' : X → ℝ) (ψ ψ' : Y → ℝ) (s : Set X) : regionBetweenMap g φ φ' ψ ψ' '' Set.graphOn φ s = Set.graphOn ψ (g '' s)

On the graph of the lower source endpoint, the band map is the graph map of the lower target endpoint over g.

theorem TauCeti.image_regionBetweenMap_graphOn_upper {X : Type u_1} {Y : Type u_2} {g : X → Y} {φ φ' : X → ℝ} {ψ ψ' : Y → ℝ} {s : Set X} (h : ∀ x ∈ s, φ x = φ' x → ψ (g x) = ψ' (g x)) : regionBetweenMap g φ φ' ψ ψ' '' Set.graphOn φ' s = Set.graphOn ψ' (g '' s)

On the graph of the upper source endpoint, the band map is the graph map of the upper target endpoint over g, provided collapsed source fibres lie over collapsed target fibres.

theorem TauCeti.eqOn_regionBetweenMap {X : Type u_1} {Y : Type u_2} {s : Set X} {g₁ g₂ : X → Y} {φ₁ φ₁' φ₂ φ₂' : X → ℝ} {ψ₁ ψ₁' ψ₂ ψ₂' : Y → ℝ} (hg : Set.EqOn g₁ g₂ s) (hφ : Set.EqOn φ₁ φ₂ s) (hφ' : Set.EqOn φ₁' φ₂' s) (hψ : Set.EqOn ψ₁ ψ₂ (g₁ '' s)) (hψ' : Set.EqOn ψ₁' ψ₂' (g₁ '' s)) : Set.EqOn (regionBetweenMap g₁ φ₁ φ₁' ψ₁ ψ₁') (regionBetweenMap g₂ φ₂ φ₂' ψ₂ ψ₂') (Prod.fst ⁻¹' s)

Restriction compatibility: over a set s on which two sets of base and endpoint data agree, their band maps agree.

theorem TauCeti.mapsTo_regionBetweenMap_closedRegionBetween {X : Type u_1} {Y : Type u_2} {g : X → Y} {φ φ' : X → ℝ} {ψ ψ' : Y → ℝ} {s : Set X} {t : Set Y} (hg : Set.MapsTo g s t) (hψ : ∀ y ∈ t, ψ y ≤ ψ' y) : Set.MapsTo (regionBetweenMap g φ φ' ψ ψ') (closedRegionBetween φ φ' s) (closedRegionBetween ψ ψ' t)

The band map sends the closed band over s into the closed band over t.

theorem TauCeti.mapsTo_regionBetweenMap_regionBetween {X : Type u_1} {Y : Type u_2} {g : X → Y} {φ φ' : X → ℝ} {ψ ψ' : Y → ℝ} {s : Set X} {t : Set Y} (hg : Set.MapsTo g s t) (hψ : ∀ y ∈ t, ψ y < ψ' y) : Set.MapsTo (regionBetweenMap g φ φ' ψ ψ') (regionBetween φ φ' s) (regionBetween ψ ψ' t)

The band map sends the open band over s into the open band over t.

theorem TauCeti.regionBetweenMap_regionBetweenMap {X : Type u_1} {Y : Type u_2} {g : X → Y} {g' : Y → X} {φ φ' : X → ℝ} {ψ ψ' : Y → ℝ} {x : X} {r : ℝ} (hx : g' (g x) = x) (hcollapse : ψ (g x) = ψ' (g x) → φ x = φ' x) (hr : r ∈ Set.Icc (φ x) (φ' x)) : regionBetweenMap g' ψ ψ' φ φ' (regionBetweenMap g φ φ' ψ ψ' (x, r)) = (x, r)

The band map over a left inverse g' of g, with source and target endpoints exchanged, undoes the band map over g on the fibre over x, provided the source fibre over x collapses whenever the target fibre over g x does.

theorem TauCeti.invOn_regionBetweenMap {X : Type u_1} {Y : Type u_2} {g : X → Y} {g' : Y → X} {φ φ' : X → ℝ} {ψ ψ' : Y → ℝ} {s : Set X} {t : Set Y} (h : Set.InvOn g' g s t) (hg' : Set.MapsTo g' t s) (hcollapse : ∀ x ∈ s, φ x = φ' x ↔ ψ (g x) = ψ' (g x)) : Set.InvOn (regionBetweenMap g' ψ ψ' φ φ') (regionBetweenMap g φ φ' ψ ψ') (closedRegionBetween φ φ' s) (closedRegionBetween ψ ψ' t)

If g' and g are inverse on s and t, g' maps t to s, and a source fibre collapses exactly when the target fibre over it does, then the band maps over g and g' are inverse on the closed bands.

theorem TauCeti.bijOn_regionBetweenMap {X : Type u_1} {Y : Type u_2} {g : X → Y} {g' : Y → X} {φ φ' : X → ℝ} {ψ ψ' : Y → ℝ} {s : Set X} {t : Set Y} (h : Set.InvOn g' g s t) (hg : Set.MapsTo g s t) (hg' : Set.MapsTo g' t s) (hφ : ∀ x ∈ s, φ x ≤ φ' x) (hψ : ∀ y ∈ t, ψ y ≤ ψ' y) (hcollapse : ∀ x ∈ s, φ x = φ' x ↔ ψ (g x) = ψ' (g x)) : Set.BijOn (regionBetweenMap g φ φ' ψ ψ') (closedRegionBetween φ φ' s) (closedRegionBetween ψ ψ' t)

If g is a bijection from s to t with inverse g', the endpoints are ordered, and a source fibre collapses exactly when the target fibre over it does, then the band map is a bijection between the closed bands.

theorem TauCeti.bijOn_regionBetweenMap_regionBetween {X : Type u_1} {Y : Type u_2} {g : X → Y} {g' : Y → X} {φ φ' : X → ℝ} {ψ ψ' : Y → ℝ} {s : Set X} {t : Set Y} (h : Set.InvOn g' g s t) (hg : Set.MapsTo g s t) (hg' : Set.MapsTo g' t s) (hφ : ∀ x ∈ s, φ x < φ' x) (hψ : ∀ y ∈ t, ψ y < ψ' y) : Set.BijOn (regionBetweenMap g φ φ' ψ ψ') (regionBetween φ φ' s) (regionBetween ψ ψ' t)

If g is a bijection from s to t with inverse g' and the endpoints are strictly ordered, then the band map is a bijection between the open bands.

theorem TauCeti.regionBetweenMap_id {X : Type u_1} {a b : X → ℝ} {p : X × ℝ} (hp : p.2 ∈ Set.Icc (a p.1) (b p.1)) : regionBetweenMap id a b a b p = p

Interpolation with unchanged endpoints is the identity on every closed fibre, including a collapsed fibre.

theorem TauCeti.regionBetweenMap_comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (g : X → Y) (h : Y → Z) (a b : X → ℝ) (c d : Y → ℝ) (u v : Z → ℝ) (p : X × ℝ) (hcollapse : c (g p.1) = d (g p.1) → u (h (g p.1)) = v (h (g p.1))) : regionBetweenMap h c d u v (regionBetweenMap g a b c d p) = regionBetweenMap (h ∘ g) a b u v p

Successive band interpolations compose to the direct interpolation. A collapsed intermediate fibre must also collapse in the final band; no converse is needed.

theorem TauCeti.continuousOn_regionBetweenMap {X : Type u_1} {Y : Type u_2} {g : X → Y} {φ φ' : X → ℝ} {ψ ψ' : Y → ℝ} {s : Set X} {t : Set Y} [TopologicalSpace X] [TopologicalSpace Y] (hg : ContinuousOn g s) (hφ : ContinuousOn φ s) (hφ' : ContinuousOn φ' s) (hψ : ContinuousOn ψ t) (hψ' : ContinuousOn ψ' t) (hgst : Set.MapsTo g s t) (hcollapse : ∀ x ∈ s, φ x = φ' x → ψ (g x) = ψ' (g x)) : ContinuousOn (regionBetweenMap g φ φ' ψ ψ') (closedRegionBetween φ φ' s)

Continuity of the closed-band map: if the base map and the endpoints are continuous and every collapsed source fibre lies over a collapsed target fibre, then the band map is continuous on the closed band.

theorem TauCeti.isOpen_regionBetween {X : Type u_1} [TopologicalSpace X] {s : Set X} {φ φ' : X → ℝ} (hs : IsOpen s) (hφ : ContinuousOn φ s) (hφ' : ContinuousOn φ' s) : IsOpen (regionBetween φ φ' s)

The open band between continuous endpoints over an open base is open.

noncomputable def OpenPartialHomeomorph.regionBetween {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) (φ φ' : X → ℝ) (ψ ψ' : Y → ℝ) (hφ : ContinuousOn φ e.source) (hφ' : ContinuousOn φ' e.source) (hψ : ContinuousOn ψ e.target) (hψ' : ContinuousOn ψ' e.target) (hφφ' : ∀ x ∈ e.source, φ x < φ' x) (hψψ' : ∀ y ∈ e.target, ψ y < ψ' y) : OpenPartialHomeomorph (X × ℝ) (Y × ℝ)

Affine interpolation between strictly ordered continuous endpoints lifts an open partial homeomorphism of the bases to an open partial homeomorphism of their open bands.

@[simp]

theorem OpenPartialHomeomorph.regionBetween_source {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) (φ φ' : X → ℝ) (ψ ψ' : Y → ℝ) (hφ : ContinuousOn φ e.source) (hφ' : ContinuousOn φ' e.source) (hψ : ContinuousOn ψ e.target) (hψ' : ContinuousOn ψ' e.target) (hφφ' : ∀ x ∈ e.source, φ x < φ' x) (hψψ' : ∀ y ∈ e.target, ψ y < ψ' y) : (e.regionBetween φ φ' ψ ψ' hφ hφ' hψ hψ' hφφ' hψψ').source = _root_.regionBetween φ φ' e.source

@[simp]

theorem OpenPartialHomeomorph.regionBetween_target {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) (φ φ' : X → ℝ) (ψ ψ' : Y → ℝ) (hφ : ContinuousOn φ e.source) (hφ' : ContinuousOn φ' e.source) (hψ : ContinuousOn ψ e.target) (hψ' : ContinuousOn ψ' e.target) (hφφ' : ∀ x ∈ e.source, φ x < φ' x) (hψψ' : ∀ y ∈ e.target, ψ y < ψ' y) : (e.regionBetween φ φ' ψ ψ' hφ hφ' hψ hψ' hφφ' hψψ').target = _root_.regionBetween ψ ψ' e.target

@[simp]

theorem OpenPartialHomeomorph.coe_regionBetween {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) (φ φ' : X → ℝ) (ψ ψ' : Y → ℝ) (hφ : ContinuousOn φ e.source) (hφ' : ContinuousOn φ' e.source) (hψ : ContinuousOn ψ e.target) (hψ' : ContinuousOn ψ' e.target) (hφφ' : ∀ x ∈ e.source, φ x < φ' x) (hψψ' : ∀ y ∈ e.target, ψ y < ψ' y) : ↑(e.regionBetween φ φ' ψ ψ' hφ hφ' hψ hψ' hφφ' hψψ') = TauCeti.regionBetweenMap (↑e) φ φ' ψ ψ'

@[simp]

theorem OpenPartialHomeomorph.coe_regionBetween_symm {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) (φ φ' : X → ℝ) (ψ ψ' : Y → ℝ) (hφ : ContinuousOn φ e.source) (hφ' : ContinuousOn φ' e.source) (hψ : ContinuousOn ψ e.target) (hψ' : ContinuousOn ψ' e.target) (hφφ' : ∀ x ∈ e.source, φ x < φ' x) (hψψ' : ∀ y ∈ e.target, ψ y < ψ' y) : ↑(e.regionBetween φ φ' ψ ψ' hφ hφ' hψ hψ' hφφ' hψψ').symm = TauCeti.regionBetweenMap (↑e.symm) ψ ψ' φ φ'