Fibrewise radial compression

Radial compression in each real seminormed fibre sends the whole fibre bijectively onto its open unit ball. These maps preserve base points, fix the zero section, and have explicit square-root formulas and inverse identities. They are the fibre maps used to parametrize bounded bundle neighbourhoods by an entire vector bundle.

The construction uses Mathlib's OpenPartialHomeomorph.univUnitBall, by Yury Kudryashov and Oliver Nash, separately in each fibre. Regularity on a bundle total space additionally requires regularity of the fibre norm.

noncomputable def Bundle.TotalSpace.radialMap {B : Type u_1} {V : B → Type u_2} {F : Type u_3} [(b : B) → SeminormedAddCommGroup (V b)] [(b : B) → NormedSpace ℝ (V b)] (p : TotalSpace F V) : TotalSpace F V

Compress each fibre into its open unit ball, preserving the base point.

noncomputable def Bundle.TotalSpace.radialInverse {B : Type u_1} {V : B → Type u_2} {F : Type u_3} [(b : B) → SeminormedAddCommGroup (V b)] [(b : B) → NormedSpace ℝ (V b)] (p : TotalSpace F V) : TotalSpace F V

Expand the open unit ball in each fibre to the whole fibre. The inverse identities for this map hold on the open unit ball bundle.

theorem Bundle.TotalSpace.radialMap_apply {B : Type u_1} {V : B → Type u_2} {F : Type u_3} [(b : B) → SeminormedAddCommGroup (V b)] [(b : B) → NormedSpace ℝ (V b)] (p : TotalSpace F V) : p.radialMap = { proj := p.proj, snd := (√(1 + ‖p.snd‖ ^ 2))⁻¹ • p.snd }

Radial compression in fibre coordinates.

theorem Bundle.TotalSpace.radialInverse_apply {B : Type u_1} {V : B → Type u_2} {F : Type u_3} [(b : B) → SeminormedAddCommGroup (V b)] [(b : B) → NormedSpace ℝ (V b)] (p : TotalSpace F V) : p.radialInverse = { proj := p.proj, snd := (√(1 - ‖p.snd‖ ^ 2))⁻¹ • p.snd }

Radial expansion in fibre coordinates.

@[simp]

theorem Bundle.TotalSpace.norm_radialMap_lt_one {B : Type u_1} {V : B → Type u_2} {F : Type u_3} [(b : B) → SeminormedAddCommGroup (V b)] [(b : B) → NormedSpace ℝ (V b)] (p : TotalSpace F V) : ‖p.radialMap.snd‖ < 1

Every compressed vector lies in the open unit ball of its fibre.

@[simp]

theorem Bundle.TotalSpace.radialMap_proj {B : Type u_1} {V : B → Type u_2} {F : Type u_3} [(b : B) → SeminormedAddCommGroup (V b)] [(b : B) → NormedSpace ℝ (V b)] (p : TotalSpace F V) : p.radialMap.proj = p.proj

Radial compression preserves the bundle projection.

@[simp]

theorem Bundle.TotalSpace.radialInverse_proj {B : Type u_1} {V : B → Type u_2} {F : Type u_3} [(b : B) → SeminormedAddCommGroup (V b)] [(b : B) → NormedSpace ℝ (V b)] (p : TotalSpace F V) : p.radialInverse.proj = p.proj

Radial expansion preserves the bundle projection.

@[simp]

theorem Bundle.TotalSpace.radialMap_zeroSection {B : Type u_1} {V : B → Type u_2} {F : Type u_3} [(b : B) → SeminormedAddCommGroup (V b)] [(b : B) → NormedSpace ℝ (V b)] (b : B) : (zeroSection F V b).radialMap = zeroSection F V b

Radial compression fixes the zero section.

@[simp]

theorem Bundle.TotalSpace.radialInverse_zeroSection {B : Type u_1} {V : B → Type u_2} {F : Type u_3} [(b : B) → SeminormedAddCommGroup (V b)] [(b : B) → NormedSpace ℝ (V b)] (b : B) : (zeroSection F V b).radialInverse = zeroSection F V b

Radial expansion fixes the zero section.

@[simp]

theorem Bundle.TotalSpace.radialInverse_map {B : Type u_1} {V : B → Type u_2} {F : Type u_3} [(b : B) → SeminormedAddCommGroup (V b)] [(b : B) → NormedSpace ℝ (V b)] (p : TotalSpace F V) : p.radialMap.radialInverse = p

Expansion undoes compression on the entire total space.

@[simp]

theorem Bundle.TotalSpace.radialMap_inverse {B : Type u_1} {V : B → Type u_2} {F : Type u_3} [(b : B) → SeminormedAddCommGroup (V b)] [(b : B) → NormedSpace ℝ (V b)] (p : TotalSpace F V) (hp : ‖p.snd‖ < 1) : p.radialInverse.radialMap = p

Compression undoes expansion on the open unit ball bundle.