English
In finite dimensions, there exists a canonical smooth bump function; every finite-dimensional real normed space supports a smooth bump.
Русский
В конечномерном пространстве существует каноническая гладкая функция-бум; любое конечномерное вещественное нормированное пространство поддерживает гладкий бум.
LaTeX
$$HasContDiffBump E$$
Lean4
instance (priority := 100) {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] :
HasContDiffBump E := by
refine ⟨⟨?_⟩⟩
borelize E
have IR : ∀ R : ℝ, 1 < R → 0 < (R - 1) / (R + 1) := by intro R hR; apply div_pos <;> linarith
exact
{ toFun := fun R x => if 1 < R then y ((R - 1) / (R + 1)) (((R + 1) / 2)⁻¹ • x) else 0
mem_Icc := fun R x => by
simp only [mem_Icc]
split_ifs with h
· refine ⟨y_nonneg _ _, y_le_one _ (IR R h)⟩
· simp only [le_refl, zero_le_one, and_self]
symmetric := fun R x => by
split_ifs
· simp only [y_neg, smul_neg]
· rfl
smooth :=
by
suffices
ContDiffOn ℝ ∞ (uncurry y ∘ fun p : ℝ × E => ((p.1 - 1) / (p.1 + 1), ((p.1 + 1) / 2)⁻¹ • p.2)) (Ioi 1 ×ˢ univ)
by
apply this.congr
rintro ⟨R, x⟩ ⟨hR : 1 < R, _⟩
simp only [hR, uncurry_apply_pair, if_true, Function.comp_apply]
apply (y_smooth E).comp
· apply ContDiffOn.prodMk
· refine (contDiffOn_fst.sub contDiffOn_const).div (contDiffOn_fst.add contDiffOn_const) ?_
rintro ⟨R, x⟩ ⟨hR : 1 < R, _⟩
apply ne_of_gt
dsimp only
linarith
· apply ContDiffOn.smul _ contDiffOn_snd
refine ((contDiffOn_fst.add contDiffOn_const).div_const _).inv ?_
rintro ⟨R, x⟩ ⟨hR : 1 < R, _⟩
apply ne_of_gt
dsimp only
linarith
· rintro ⟨R, x⟩ ⟨hR : 1 < R, _⟩
have A : 0 < (R - 1) / (R + 1) := by apply div_pos <;> linarith
have B : (R - 1) / (R + 1) < 1 := by apply (div_lt_one _).2 <;> linarith
simp only [prodMk_mem_set_prod_eq, mem_Ioo, mem_univ, and_true, A, B]
eq_one := fun R hR x hx => by
have A : 0 < R + 1 := by linarith
simp only [hR, if_true]
apply y_eq_one_of_mem_closedBall (IR R hR)
simp only [norm_smul, inv_div, mem_closedBall_zero_iff, Real.norm_eq_abs, abs_div, abs_two, abs_of_nonneg A.le]
calc
2 / (R + 1) * ‖x‖ ≤ 2 / (R + 1) := mul_le_of_le_one_right (by positivity) hx
_ = 1 - (R - 1) / (R + 1) := by field_simp; ring
support := fun R hR => by
have A : 0 < (R + 1) / 2 := by linarith
have C : (R - 1) / (R + 1) < 1 := by apply (div_lt_one _).2 <;> linarith
simp only [hR, if_true, support_comp_inv_smul₀ A.ne', y_support _ (IR R hR) C, _root_.smul_ball A.ne',
Real.norm_of_nonneg A.le, smul_zero]
refine congr (congr_arg ball (Eq.refl 0)) ?_
field_simp; ring }
