Smooth radial coordinates with variable radius

A positive C^n radius on the base identifies the entire smooth normal bundle of a Euclidean immersion with its variable-radius open ball bundle. The identification preserves base points and fixes the zero section. Unlike a constant radius, a variable radius can shrink towards infinity on a noncompact submanifold, as needed to parametrize its tubular neighbourhood by the whole normal bundle.

The construction composes normalBundleRadialPartialDiffeomorph at unit radius with vectorBundleScalarDiffeomorph; it uses their smoothness and inverse laws rather than reproving the radial calculus. As with the fixed-radius construction, install normalFiberBundle locally to use the resulting partial diffeomorphism.

Reference: J. M. Lee, Introduction to Smooth Manifolds, second edition, Theorem 6.24.

noncomputable def TauCeti.normalBundleRadialPartialDiffeomorphOfRadius {V : Type u_1} {E : Type u_2} {H : Type u_3} {M : Type u_4} {F : Type u_5} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] [FiniteDimensional ℝ V] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [I.Boundaryless] {n : ℕ∞} [IsManifold I (↑n + 1) M] {f : M → V} (hf : ContMDiff I (modelWithCornersSelf ℝ V) (↑n + 1) f) (himm : ∀ (x : M), Function.Injective ⇑(mfderiv% f x)) (hdim : Module.finrank ℝ F = Module.finrank ℝ V - Module.finrank ℝ E) {r : M → ℝ} (hr : ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑n) r) (hrpos : ∀ (x : M), 0 < r x) : PartialDiffeomorph (I.prod (modelWithCornersSelf ℝ F)) (I.prod (modelWithCornersSelf ℝ F)) (Bundle.TotalSpace F fun (x : M) => ↥(normalSubspace I f x)) (Bundle.TotalSpace F fun (x : M) => ↥(normalSubspace I f x)) ↑n

Radial compression followed by fibrewise rescaling identifies the whole smooth normal bundle with its open ball bundle of positive C^n radius r.

@[simp]

theorem TauCeti.normalBundleRadialPartialDiffeomorphOfRadius_source {V : Type u_1} {E : Type u_2} {H : Type u_3} {M : Type u_4} {F : Type u_5} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] [FiniteDimensional ℝ V] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [I.Boundaryless] {n : ℕ∞} [IsManifold I (↑n + 1) M] {f : M → V} (hf : ContMDiff I (modelWithCornersSelf ℝ V) (↑n + 1) f) (himm : ∀ (x : M), Function.Injective ⇑(mfderiv% f x)) (hdim : Module.finrank ℝ F = Module.finrank ℝ V - Module.finrank ℝ E) {r : M → ℝ} (hr : ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑n) r) (hrpos : ∀ (x : M), 0 < r x) : (normalBundleRadialPartialDiffeomorphOfRadius hf himm hdim hr hrpos).source = Set.univ

Variable-radius radial coordinates are defined on the entire normal bundle.

@[simp]

theorem TauCeti.normalBundleRadialPartialDiffeomorphOfRadius_target {V : Type u_1} {E : Type u_2} {H : Type u_3} {M : Type u_4} {F : Type u_5} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] [FiniteDimensional ℝ V] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [I.Boundaryless] {n : ℕ∞} [IsManifold I (↑n + 1) M] {f : M → V} (hf : ContMDiff I (modelWithCornersSelf ℝ V) (↑n + 1) f) (himm : ∀ (x : M), Function.Injective ⇑(mfderiv% f x)) (hdim : Module.finrank ℝ F = Module.finrank ℝ V - Module.finrank ℝ E) {r : M → ℝ} (hr : ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑n) r) (hrpos : ∀ (x : M), 0 < r x) : (normalBundleRadialPartialDiffeomorphOfRadius hf himm hdim hr hrpos).target = {p : Bundle.TotalSpace F fun (x : M) => ↥(normalSubspace I f x) | ‖↑p.snd‖ < r p.proj}

The target consists exactly of normal vectors shorter than the radius at their base.

@[simp]

theorem TauCeti.normalBundleRadialPartialDiffeomorphOfRadius_apply {V : Type u_1} {E : Type u_2} {H : Type u_3} {M : Type u_4} {F : Type u_5} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] [FiniteDimensional ℝ V] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [I.Boundaryless] {n : ℕ∞} [IsManifold I (↑n + 1) M] {f : M → V} (hf : ContMDiff I (modelWithCornersSelf ℝ V) (↑n + 1) f) (himm : ∀ (x : M), Function.Injective ⇑(mfderiv% f x)) (hdim : Module.finrank ℝ F = Module.finrank ℝ V - Module.finrank ℝ E) {r : M → ℝ} (hr : ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑n) r) (hrpos : ∀ (x : M), 0 < r x) (p : Bundle.TotalSpace F fun (x : M) => ↥(normalSubspace I f x)) : ↑(normalBundleRadialPartialDiffeomorphOfRadius hf himm hdim hr hrpos).toPartialEquiv p = normalBundleRadialMap f (r p.proj) p

Compression uses the fixed-radius fibre formula with the radius at the base point.

@[simp]

theorem TauCeti.normalBundleRadialPartialDiffeomorphOfRadius_symm_apply {V : Type u_1} {E : Type u_2} {H : Type u_3} {M : Type u_4} {F : Type u_5} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] [FiniteDimensional ℝ V] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [I.Boundaryless] {n : ℕ∞} [IsManifold I (↑n + 1) M] {f : M → V} (hf : ContMDiff I (modelWithCornersSelf ℝ V) (↑n + 1) f) (himm : ∀ (x : M), Function.Injective ⇑(mfderiv% f x)) (hdim : Module.finrank ℝ F = Module.finrank ℝ V - Module.finrank ℝ E) {r : M → ℝ} (hr : ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑n) r) (hrpos : ∀ (x : M), 0 < r x) (p : Bundle.TotalSpace F fun (x : M) => ↥(normalSubspace I f x)) : ↑(normalBundleRadialPartialDiffeomorphOfRadius hf himm hdim hr hrpos).symm p = normalBundleRadialInverse f (r p.proj) p

The inverse expands using the radius at the same base point.