Smooth radii inside product neighbourhoods

A neighbourhood of a constant section in M × V contains a closed ball of positive smooth radius in each fibre, and the radius can be chosen below any positive lower semicontinuous bound. The radius can tend to zero at infinity; no uniform radius or compactness of M is required. This is the shrinking step used to fit normal disc bundles inside prescribed neighbourhoods before constructing tubular coordinates.

The construction uses Mathlib's convex-valued smooth selection theorem exists_contMDiffMap_forall_mem_convex_of_local_const.

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

theorem TauCeti.exists_contMDiffMap_closedBall_subset {E : Type u_1} {H : Type u_2} {M : Type u_3} {V : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [T2Space M] [SigmaCompactSpace M] [PseudoMetricSpace V] {U : Set (M × V)} {v₀ : V} (hU : ∀ (x : M), U ∈ nhds (x, v₀)) {ε : M → ℝ} (hε : LowerSemicontinuous ε) (hεpos : ∀ (x : M), 0 < ε x) : ∃ (r : ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ↑⊤), (∀ (x : M), 0 < r x) ∧ (∀ (x : M), r x < ε x) ∧ ∀ (x : M), ∀ v ∈ Metric.closedBall v₀ (r x), (x, v) ∈ U

Every neighbourhood of a constant section contains fibrewise closed balls of a positive smooth radius smaller than any given positive lower semicontinuous bound. The second factor can be any pseudometric space.