English
The function y is smoothly dependent on both radius and center, giving a global smooth bump construction.
Русский
Функция y гладко зависит от радиуса и центра, обеспечивая глобальную гладкую конструкцию бум.
LaTeX
$$y is smooth in both D and x$$
Lean4
theorem y_smooth : ContDiffOn ℝ ∞ (uncurry y) (Ioo (0 : ℝ) 1 ×ˢ (univ : Set E)) :=
by
have hs : IsOpen (Ioo (0 : ℝ) (1 : ℝ)) := isOpen_Ioo
have hk : IsCompact (closedBall (0 : E) 1) := ProperSpace.isCompact_closedBall _ _
refine contDiffOn_convolution_left_with_param (lsmul ℝ ℝ) hs hk ?_ ?_ ?_
· rintro p x hp hx
simp only [w, mul_inv_rev, Algebra.id.smul_eq_mul, mul_eq_zero, inv_eq_zero]
right
contrapose! hx
have : p⁻¹ • x ∈ support u := mem_support.2 hx
simp only [u_support, norm_smul, mem_ball_zero_iff, Real.norm_eq_abs, abs_inv, abs_of_nonneg hp.1.le,
← div_eq_inv_mul, div_lt_one hp.1] at this
rw [mem_closedBall_zero_iff]
exact this.le.trans hp.2.le
· exact (locallyIntegrable_const _).indicator measurableSet_closedBall
· apply ContDiffOn.mul
· norm_cast
refine
(contDiffOn_const.mul ?_).inv fun x hx =>
ne_of_gt (mul_pos (u_int_pos E) (pow_pos (abs_pos_of_pos hx.1.1) (finrank ℝ E)))
apply ContDiffOn.pow
simp_rw [← Real.norm_eq_abs]
apply ContDiffOn.norm ℝ
· exact contDiffOn_fst
· intro x hx; exact ne_of_gt hx.1.1
· apply (u_smooth E).comp_contDiffOn
exact ContDiffOn.smul (contDiffOn_fst.inv fun x hx => ne_of_gt hx.1.1) contDiffOn_snd
