Radial coordinates on the cube

Mathlib's generalized loops Ω^ N X x are continuous maps I^N → X that are constant on the cube boundary Cube.boundary N = {y | ∃ i, y i = 0 ∨ y i = 1}. Arguments that shrink a generalized loop into the middle of the cube and fill the resulting collar — the standard way to move the base point of a higher homotopy group along a path — need a numerical grip on how far a cube point is from the boundary. This file supplies it, for a finite index type.

The sup distance to the centre is the right measure: on I^N with N finite, the product metric is the sup metric, so

• TauCeti.cubeRadius z = 2 * dist z TauCeti.cubeCenter

is continuous for free, takes values in [0, 1], vanishes at the centre, and equals 1 exactly on the boundary (TauCeti.cubeRadius_eq_one_iff). Radial rescaling by a factor s is TauCeti.cubeScale, defined with Set.projIcc so that it is total and jointly continuous, and it multiplies the radius by s as long as the result still fits in the cube (TauCeti.cubeRadius_cubeScale). In particular a point of radius r > 0 is scaled by 1 / r onto the boundary, which is what makes the collar constructions glue continuously.

Main declarations

• TauCeti.cubeCenter, TauCeti.cubeRadius: the centre of I^N and the sup radius around it.
• TauCeti.cubeRadius_le_one and TauCeti.cubeRadius_eq_one_iff: the radius is at most one, with equality exactly on Cube.boundary N.
• TauCeti.cubeScale: radial rescaling of a cube point, and TauCeti.cubeRadius_cubeScale: it scales the radius.

References

This supplies the cube geometry behind the base-point-change isomorphisms of higher homotopy groups requested in TauCetiRoadmap/UniversalCovers/README.md, Stage 3, item 9.

The centre of the cube and radial rescaling

noncomputable def TauCeti.cubeCenter {N : Type u_1} : N → ↑unitInterval

The centre of the cube I^N, all of whose coordinates are 1 / 2.

Equations

• TauCeti.cubeCenter x✝ = ⟨1 / 2, TauCeti.cubeCenter._proof_2✝⟩

@[simp]

theorem TauCeti.cubeCenter_apply {N : Type u_1} (i : N) : ↑(cubeCenter i) = 1 / 2

noncomputable def TauCeti.cubeScale {N : Type u_1} (s : ℝ) (z : N → ↑unitInterval) : N → ↑unitInterval

Radial rescaling of a cube point about the centre by a factor s, clamped back into the cube so that it is total and jointly continuous. It agrees with the honest rescaling whenever the rescaled point still lies in the cube; see TauCeti.cubeScale_apply_coe.

Equations

• TauCeti.cubeScale s z i = Set.projIcc 0 1 TauCeti.cubeScale._proof_1✝ (1 / 2 + (↑(z i) - 1 / 2) * s)

theorem TauCeti.continuous_cubeScale {N : Type u_1} : Continuous fun (p : ℝ × (N → ↑unitInterval)) => cubeScale p.1 p.2

@[simp]

theorem TauCeti.cubeScale_one {N : Type u_1} (z : N → ↑unitInterval) : cubeScale 1 z = z

noncomputable def TauCeti.cubeRadius {N : Type u_1} [Fintype N] (z : N → ↑unitInterval) : ℝ

The sup radius of a cube point around the centre of the cube, normalised so that the boundary has radius one.

Equations

• TauCeti.cubeRadius z = 2 * dist z TauCeti.cubeCenter

theorem TauCeti.cubeRadius_def {N : Type u_1} [Fintype N] (z : N → ↑unitInterval) : cubeRadius z = 2 * dist z cubeCenter

theorem TauCeti.continuous_cubeRadius {N : Type u_1} [Fintype N] : Continuous cubeRadius

theorem TauCeti.cubeRadius_nonneg {N : Type u_1} [Fintype N] (z : N → ↑unitInterval) : 0 ≤ cubeRadius z

theorem TauCeti.dist_apply_cubeCenter {N : Type u_1} (z : N → ↑unitInterval) (i : N) : dist (z i) (cubeCenter i) = |↑(z i) - 1 / 2|

theorem TauCeti.abs_sub_half_le_cubeRadius {N : Type u_1} [Fintype N] (z : N → ↑unitInterval) (i : N) : |↑(z i) - 1 / 2| ≤ cubeRadius z / 2

theorem TauCeti.cubeRadius_le_one {N : Type u_1} [Fintype N] (z : N → ↑unitInterval) : cubeRadius z ≤ 1

theorem TauCeti.cubeRadius_eq_one_iff {N : Type u_1} [Fintype N] (z : N → ↑unitInterval) : cubeRadius z = 1 ↔ z ∈ Cube.boundary N

A cube point has radius one exactly when it lies on the boundary of the cube.

theorem TauCeti.cubeScale_apply_coe {N : Type u_1} [Fintype N] {s : ℝ} (hs : 0 ≤ s) {z : N → ↑unitInterval} (h : s * cubeRadius z ≤ 1) (i : N) : ↑(cubeScale s z i) = 1 / 2 + (↑(z i) - 1 / 2) * s

Radial rescaling is honest, that is, the clamping in TauCeti.cubeScale is inactive, as soon as the rescaled radius still fits inside the cube.

theorem TauCeti.cubeRadius_cubeScale {N : Type u_1} [Fintype N] {s : ℝ} (hs : 0 ≤ s) {z : N → ↑unitInterval} (h : s * cubeRadius z ≤ 1) : cubeRadius (cubeScale s z) = s * cubeRadius z

Rescaling radially by s multiplies the radius by s, provided the rescaled point still fits in the cube.