"Gauge rescale" homeomorphism between convex sets

Given two convex von Neumann bounded neighbourhoods of the origin in a real topological vector space, we construct a homeomorphism gaugeRescaleHomeomorph that sends the interior, the closure, and the frontier of one set to the interior, the closure, and the frontier of the other set.

def gaugeRescale {E : Type u_1} [AddCommGroup E] [Module ℝ E] (s t : Set E) (x : E) : E

The gauge rescale map gaugeRescale s t sends each point x to the point y on the same ray that has the same gauge w.r.t. t as x has w.r.t. s.

The characteristic property is satisfied if gauge t x ≠ 0, see gauge_gaugeRescale'. In particular, it is satisfied for all x, provided that t is absorbent and von Neumann bounded.

Equations

• gaugeRescale s t x = (gauge s x / gauge t x) • x

theorem gaugeRescale_def {E : Type u_1} [AddCommGroup E] [Module ℝ E] (s t : Set E) (x : E) : gaugeRescale s t x = (gauge s x / gauge t x) • x

@[simp]

theorem gaugeRescale_zero {E : Type u_1} [AddCommGroup E] [Module ℝ E] (s t : Set E) : gaugeRescale s t 0 = 0

theorem gaugeRescale_smul {E : Type u_1} [AddCommGroup E] [Module ℝ E] (s t : Set E) {c : ℝ} (hc : 0 ≤ c) (x : E) : gaugeRescale s t (c • x) = c • gaugeRescale s t x

theorem gauge_gaugeRescale' {E : Type u_1} [AddCommGroup E] [Module ℝ E] (s : Set E) {t : Set E} {x : E} (hx : gauge t x ≠ 0) : gauge t (gaugeRescale s t x) = gauge s x

theorem gauge_gaugeRescale_le {E : Type u_1} [AddCommGroup E] [Module ℝ E] (s t : Set E) (x : E) : gauge t (gaugeRescale s t x) ≤ gauge s x

theorem gaugeRescale_self_apply {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [T1Space E] {s : Set E} (hsa : Absorbent ℝ s) (hsb : Bornology.IsVonNBounded ℝ s) (x : E) : gaugeRescale s s x = x

theorem gaugeRescale_self {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [T1Space E] {s : Set E} (hsa : Absorbent ℝ s) (hsb : Bornology.IsVonNBounded ℝ s) : gaugeRescale s s = id

theorem gauge_gaugeRescale {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [T1Space E] (s : Set E) {t : Set E} (hta : Absorbent ℝ t) (htb : Bornology.IsVonNBounded ℝ t) (x : E) : gauge t (gaugeRescale s t x) = gauge s x

theorem gaugeRescale_gaugeRescale {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [T1Space E] {s t u : Set E} (hta : Absorbent ℝ t) (htb : Bornology.IsVonNBounded ℝ t) (x : E) : gaugeRescale t u (gaugeRescale s t x) = gaugeRescale s u x

def gaugeRescaleEquiv {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [T1Space E] (s t : Set E) (hsa : Absorbent ℝ s) (hsb : Bornology.IsVonNBounded ℝ s) (hta : Absorbent ℝ t) (htb : Bornology.IsVonNBounded ℝ t) : E ≃ E

gaugeRescale bundled as an Equiv.

Equations

• gaugeRescaleEquiv s t hsa hsb hta htb = { toFun := gaugeRescale s t, invFun := gaugeRescale t s, left_inv := ⋯, right_inv := ⋯ }

theorem mapsTo_gaugeRescale_interior {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul ℝ E] {s t : Set E} (h₀ : t ∈ nhds 0) (hc : Convex ℝ t) : Set.MapsTo (gaugeRescale s t) (interior s) (interior t)

theorem mapsTo_gaugeRescale_closure {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul ℝ E] {s t : Set E} (hsc : Convex ℝ s) (hs₀ : s ∈ nhds 0) (htc : Convex ℝ t) (ht₀ : 0 ∈ t) (hta : Absorbent ℝ t) : Set.MapsTo (gaugeRescale s t) (closure s) (closure t)

theorem continuous_gaugeRescale {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul ℝ E] [T1Space E] {s t : Set E} (hs : Convex ℝ s) (hs₀ : s ∈ nhds 0) (ht : Convex ℝ t) (ht₀ : t ∈ nhds 0) (htb : Bornology.IsVonNBounded ℝ t) : Continuous (gaugeRescale s t)

def gaugeRescaleHomeomorph {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul ℝ E] [T1Space E] (s t : Set E) (hsc : Convex ℝ s) (hs₀ : s ∈ nhds 0) (hsb : Bornology.IsVonNBounded ℝ s) (htc : Convex ℝ t) (ht₀ : t ∈ nhds 0) (htb : Bornology.IsVonNBounded ℝ t) : E ≃ₜ E

gaugeRescale bundled as a Homeomorph.

Equations

• gaugeRescaleHomeomorph s t hsc hs₀ hsb htc ht₀ htb = { toEquiv := gaugeRescaleEquiv s t ⋯ hsb ⋯ htb, continuous_toFun := ⋯, continuous_invFun := ⋯ }

theorem image_gaugeRescaleHomeomorph_interior {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul ℝ E] [T1Space E] {s t : Set E} (hsc : Convex ℝ s) (hs₀ : s ∈ nhds 0) (hsb : Bornology.IsVonNBounded ℝ s) (htc : Convex ℝ t) (ht₀ : t ∈ nhds 0) (htb : Bornology.IsVonNBounded ℝ t) : ⇑(gaugeRescaleHomeomorph s t hsc hs₀ hsb htc ht₀ htb) '' interior s = interior t

theorem image_gaugeRescaleHomeomorph_closure {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul ℝ E] [T1Space E] {s t : Set E} (hsc : Convex ℝ s) (hs₀ : s ∈ nhds 0) (hsb : Bornology.IsVonNBounded ℝ s) (htc : Convex ℝ t) (ht₀ : t ∈ nhds 0) (htb : Bornology.IsVonNBounded ℝ t) : ⇑(gaugeRescaleHomeomorph s t hsc hs₀ hsb htc ht₀ htb) '' closure s = closure t

theorem exists_homeomorph_image_eq {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul ℝ E] [T1Space E] {s t : Set E} (hsc : Convex ℝ s) (hsne : (interior s).Nonempty) (hsb : Bornology.IsVonNBounded ℝ s) (hst : Convex ℝ t) (htne : (interior t).Nonempty) (htb : Bornology.IsVonNBounded ℝ t) : ∃ (e : E ≃ₜ E), ⇑e '' interior s = interior t ∧ ⇑e '' closure s = closure t ∧ ⇑e '' frontier s = frontier t

Given two convex bounded sets in a topological vector space with nonempty interiors, there exists a homeomorphism of the ambient space that sends the interior, the closure, and the frontier of one set to the interior, the closure, and the frontier of the other set.

In particular, if both s and t are open set or both s and t are closed sets, then e maps s to t.

theorem exists_homeomorph_image_interior_closure_frontier_eq_unitBall {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} (hc : Convex ℝ s) (hne : (interior s).Nonempty) (hb : Bornology.IsBounded s) : ∃ (h : E ≃ₜ E), ⇑h '' interior s = Metric.ball 0 1 ∧ ⇑h '' closure s = Metric.closedBall 0 1 ∧ ⇑h '' frontier s = Metric.sphere 0 1

If s is a convex bounded set with a nonempty interior in a real normed space, then there is a homeomorphism of the ambient space to itself that sends the interior of s to the unit open ball and the closure of s to the unit closed ball.