English
The family y(D) is smoothly dependent on the parameter D in a suitable open set, yielding a smooth bump construction parameterized by D.
Русский
Семейство y(D) гладко зависит от параметра D на соответствующем открытом множестве, образуя гладкую конструкцию бум-подстановки зависимую от D.
LaTeX
$$ContDiffForAll D: open set, y(D) is smooth in D$$
Lean4
theorem y_le_one {D : ℝ} (x : E) (Dpos : 0 < D) : y D x ≤ 1 :=
by
have A : (w D ⋆[lsmul ℝ ℝ, μ] φ) x ≤ (w D ⋆[lsmul ℝ ℝ, μ] 1) x :=
by
apply
convolution_mono_right_of_nonneg _ (w_nonneg D) (indicator_le_self' fun x _ => zero_le_one) fun _ => zero_le_one
refine ((w_compact_support E Dpos).convolutionExists_left _ ?_ (locallyIntegrable_const (1 : ℝ)) x).integrable
exact continuous_const.mul ((u_continuous E).comp (continuous_id.const_smul _))
have B : (w D ⋆[lsmul ℝ ℝ, μ] fun _ => (1 : ℝ)) x = 1 := by
simp only [convolution, mul_one, lsmul_apply, Algebra.id.smul_eq_mul, w_integral E Dpos]
exact A.trans (le_of_eq B)
