English
There is an instance of a smooth bump in any finite-dimensional real normed space.
Русский
Существование гладкого бум-подстановки в любом конечномерном вещественном нормированном пространстве.
LaTeX
$$HasContDiffBump E$$
Lean4
/-- A base bump function in an inner product space. This construction works in any space with a
norm smooth away from zero but we do not have a typeclass for this. -/
noncomputable def ofInnerProductSpace : ContDiffBumpBase E
where
toFun R x := smoothTransition ((R - ‖x‖) / (R - 1))
mem_Icc _ _ := ⟨smoothTransition.nonneg _, smoothTransition.le_one _⟩
symmetric _ _ := by simp only [norm_neg]
smooth := by
rintro ⟨R, x⟩ ⟨hR : 1 < R, -⟩
apply ContDiffAt.contDiffWithinAt
rw [← sub_pos] at hR
rcases eq_or_ne x 0 with rfl | hx
· have A : ContinuousAt (fun p : ℝ × E ↦ (p.1 - ‖p.2‖) / (p.1 - 1)) (R, 0) :=
(continuousAt_fst.sub continuousAt_snd.norm).div (continuousAt_fst.sub continuousAt_const) hR.ne'
have B : ∀ᶠ p in 𝓝 (R, (0 : E)), 1 ≤ (p.1 - ‖p.2‖) / (p.1 - 1) :=
A.eventually <| le_mem_nhds <| (one_lt_div hR).2 <| sub_lt_sub_left (by simp) _
refine (contDiffAt_const (c := 1)).congr_of_eventuallyEq <| B.mono fun _ ↦ smoothTransition.one_of_one_le
· refine smoothTransition.contDiffAt.comp _ (ContDiffAt.div ?_ ?_ hR.ne')
· exact contDiffAt_fst.sub (contDiffAt_snd.norm ℝ hx)
· exact contDiffAt_fst.sub contDiffAt_const
eq_one _ hR _ hx := smoothTransition.one_of_one_le <| (one_le_div <| sub_pos.2 hR).2 <| sub_le_sub_left hx _
support R
hR := by
ext x
rw [mem_support, Ne, smoothTransition.zero_iff_nonpos, not_le, mem_ball_zero_iff]
simp [hR]
