Graphs and bands of affine functions

Over a simplex convexHull ℝ s of a real vector space, the graph of an affine function and the closed band TauCeti.closedRegionBetween a b (convexHull ℝ s) between two ordered affine functions a ≤ b are convex polytopes. These are the rectilinear cells of Łojasiewicz's triangulation of semianalytic sets: the cells whose simplicial subdivision (Geometry.SimplicialComplex.exists_subdivision) produces the triangulating complex. This file describes them in the terms that subdivision needs.

• AffineMap.graphOn_convexHull: the graph of an affine map over the convex hull of s is the convex hull of its graph over s. Over a simplex, the graph cell is the simplex spanned by the graph points over its vertices.
• TauCeti.closedRegionBetween_convexHull: if a ≤ b on s, the closed band between a and b over the convex hull of s is the convex hull of the lower vertices (x, a x) and the upper vertices (x, b x), x ∈ s. Over a finite set s it is therefore a polytope, hence compact (TauCeti.isCompact_closedRegionBetween_convexHull); where a = b it collapses to the graph (TauCeti.closedRegionBetween_self).
• TauCeti.graphOn_inter_prod_nonempty, TauCeti.graphOn_inter_prod_nonempty_of_le: by the intermediate value theorem, the graph of a continuous function crosses a box B ×ˢ Icc l r over a convex set B whenever the function takes values on both sides of it over B. In particular, of two bands meeting the box one above the other, if the lower graph of the upper band misses the box, then the upper graph of the lower band meets it.
• ContinuousAffineMap.intrinsicInterior_graphOn, ContinuousAffineMap.intrinsicFrontier_graphOn: the intrinsic interior of the graph of a continuous affine map lies over the intrinsic interior of its domain, and, for a closed domain, its intrinsic frontier lies over the intrinsic frontier of the domain.
• TauCeti.intrinsicInterior_closedRegionBetween: if a ≤ b on s, with a < b somewhere on s, the intrinsic interior of the closed band is the open band over the intrinsic interior of s. For closed s, its intrinsic frontier therefore consists of the lower graph, the upper graph and the closed band over the intrinsic frontier of s (TauCeti.intrinsicFrontier_closedRegionBetween).
• TauCeti.closedRegionBetween_convexHull_subset_of_le: the closed band over the convex hull of a subset t ⊆ s lies in a band over the convex hull of s whose bounds lie beyond it on t.

References

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

theorem AffineMap.graphOn_convexHull {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] (f : E →ᵃ[𝕜] F) (s : Set E) : Set.graphOn (⇑f) ((convexHull 𝕜) s) = (convexHull 𝕜) (Set.graphOn (⇑f) s)

The graph of an affine map over the convex hull of s is the convex hull of its graph over s.

theorem ConvexOn.convex_closedRegionBetween {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f g : E → ℝ} {s : Set E} (hf : ConvexOn ℝ s f) (hg : ConcaveOn ℝ s g) : Convex ℝ (TauCeti.closedRegionBetween f g s)

The closed band between a convex function and a concave function over a convex set is convex.

theorem TauCeti.closedRegionBetween_convexHull {E : Type u_1} [AddCommGroup E] [Module ℝ E] {a b : E →ᵃ[ℝ] ℝ} {s : Set E} (hab : ∀ x ∈ s, a x ≤ b x) : closedRegionBetween (⇑a) (⇑b) ((convexHull ℝ) s) = (convexHull ℝ) (Set.graphOn (⇑a) s ∪ Set.graphOn (⇑b) s)

Vertex description of a rectilinear band. If a ≤ b on s, the closed band between the affine functions a and b over the convex hull of s is the convex hull of the lower vertices (x, a x) and the upper vertices (x, b x) for x ∈ s.

theorem TauCeti.isCompact_closedRegionBetween_convexHull {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] {a b : E →ᵃ[ℝ] ℝ} {s : Set E} (hs : s.Finite) (hab : ∀ x ∈ s, a x ≤ b x) : IsCompact (closedRegionBetween (⇑a) (⇑b) ((convexHull ℝ) s))

Over the convex hull of a finite set s, the closed band between two affine functions with a ≤ b on s is compact: it is the convex hull of finitely many vertices.

theorem TauCeti.graphOn_inter_prod_nonempty {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul ℝ E] {s B : Set E} (hs : Convex ℝ s) (hB : Convex ℝ B) {f : E → ℝ} (hf : ContinuousOn f s) {x₁ x₂ : E} {y l r : ℝ} (hx₁ : x₁ ∈ s) (hx₂ : x₂ ∈ s) (hB₁ : x₁ ∈ B) (hB₂ : x₂ ∈ B) (hf₁ : f x₁ ≤ y) (hf₂ : y ≤ f x₂) (hy : y ∈ Set.Icc l r) : (Set.graphOn f s ∩ B ×ˢ Set.Icc l r).Nonempty

A function continuous on a convex set s, taking values on both sides of y ∈ Icc l r at two points of the intersection of s with a convex set B, has its graph over s meeting the box B ×ˢ Icc l r.

theorem TauCeti.graphOn_inter_prod_nonempty_of_le {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul ℝ E] {s B : Set E} (hs : Convex ℝ s) (hB : Convex ℝ B) {a₁ b₁ a₂ b₂ : E → ℝ} (hb₁ : ContinuousOn b₁ s) {l r : ℝ} (h : ∀ x ∈ s, b₁ x ≤ a₂ x) (hU₁ : (closedRegionBetween a₁ b₁ s ∩ B ×ˢ Set.Icc l r).Nonempty) (hU₂ : (closedRegionBetween a₂ b₂ s ∩ B ×ˢ Set.Icc l r).Nonempty) (hna₂ : ¬(Set.graphOn a₂ s ∩ B ×ˢ Set.Icc l r).Nonempty) : (Set.graphOn b₁ s ∩ B ×ˢ Set.Icc l r).Nonempty

If two bands over a convex set s meet a box B ×ˢ Icc l r over a convex set B, the first lying below the second, and the lower graph of the second band misses the box, then the graph of the upper function of the first band crosses the box, provided that function is continuous on s.

Intrinsic interiors and frontiers of graphs

@[simp]

theorem ContinuousAffineMap.intrinsicInterior_graphOn {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [Ring 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [IsTopologicalAddGroup F] [IsTopologicalAddGroup E] (f : E →ᴬ[𝕜] F) (s : Set E) : intrinsicInterior 𝕜 (Set.graphOn (⇑f) s) = Set.graphOn (⇑f) (intrinsicInterior 𝕜 s)

The intrinsic interior of the graph of a continuous affine map over s is its graph over the intrinsic interior of s.

theorem ContinuousAffineMap.intrinsicFrontier_graphOn {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [Ring 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [IsTopologicalAddGroup F] [IsTopologicalAddGroup E] (f : E →ᴬ[𝕜] F) [T1Space F] {s : Set E} (hs : IsClosed s) : intrinsicFrontier 𝕜 (Set.graphOn (⇑f) s) = Set.graphOn (⇑f) (intrinsicFrontier 𝕜 s)

The intrinsic frontier of the graph of a continuous affine map over a closed set s is its graph over the intrinsic frontier of s.

Intrinsic interiors and frontiers of bands

theorem TauCeti.intrinsicInterior_closedRegionBetween {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : E →ᴬ[ℝ] ℝ} {s : Set E} (hab : ∀ x ∈ s, a x ≤ b x) (h : ∃ x ∈ s, a x < b x) : intrinsicInterior ℝ (closedRegionBetween (⇑a) (⇑b) s) = regionBetween (⇑a) (⇑b) (intrinsicInterior ℝ s)

Intrinsic interior of a band. If a ≤ b on s, with a < b somewhere on s, the intrinsic interior of the closed band between the continuous affine functions a and b over s is the open band over the intrinsic interior of s.

theorem TauCeti.intrinsicFrontier_closedRegionBetween {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : E →ᴬ[ℝ] ℝ} {s : Set E} (hs : IsClosed s) (hab : ∀ x ∈ s, a x ≤ b x) (h : ∃ x ∈ s, a x < b x) : intrinsicFrontier ℝ (closedRegionBetween (⇑a) (⇑b) s) = Set.graphOn (⇑a) s ∪ Set.graphOn (⇑b) s ∪ closedRegionBetween (⇑a) (⇑b) (intrinsicFrontier ℝ s)

Intrinsic frontier of a band. If a ≤ b on a closed set s, with a < b somewhere on s, the intrinsic frontier of the closed band between the continuous affine functions a and b over s consists of the graphs of a and b over s and the closed band over the intrinsic frontier of s.

theorem TauCeti.closedRegionBetween_convexHull_subset_of_le {E : Type u_1} [AddCommGroup E] [Module ℝ E] {s t : Set E} {a b c d : E →ᵃ[ℝ] ℝ} (hts : t ⊆ s) (hac : ∀ v ∈ t, a v ≤ c v) (hdb : ∀ v ∈ t, d v ≤ b v) : closedRegionBetween (⇑c) (⇑d) ((convexHull ℝ) t) ⊆ closedRegionBetween (⇑a) (⇑b) ((convexHull ℝ) s)

The closed band between two affine functions over the convex hull of t ⊆ s lies in the closed band between two affine functions over the convex hull of s that bound them on t.