theorem IsSmoothApproximationNonneg.is_l_smooth_on_nonneg_weighted_sum {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {f1 f2 : E → ℝ} {L1 L2 gamma1 gamma2 : NNReal} (hs1 : is_l_smooth_on f1 Set.univ L1) (hs2 : is_l_smooth_on f2 Set.univ L2) : is_l_smooth_on (fun (x : E) => ↑gamma1 * f1 x + ↑gamma2 * f2 x) Set.univ (gamma1 * L1 + gamma2 * L2)

Helper for Theorem 10.46: a nonnegative weighted sum of globally smooth functions is globally smooth, with smoothness constant given by the same weighted sum.

theorem IsSmoothApproximationNonneg.fderiv_comp_continuousAffineMap {E : Type u} {V : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {f : V → ℝ} {φ : E →ᴬ[ℝ] V} {x : E} (hf : DifferentiableAt ℝ f (φ x)) : fderiv ℝ (fun (z : E) => f (φ z)) x = fderiv ℝ f (φ x) ∘SL φ.contLinear

Helper for Theorem 10.46: differentiating a real-valued function after precomposition by a continuous affine map amounts to composing the derivative with the affine map's linear part.

theorem IsSmoothApproximationNonneg.continuousAffineMap_norm_sub_le {E : Type u} {V : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (φ : E →ᴬ[ℝ] V) (x y : E) : ‖φ x - φ y‖ ≤ ‖φ.contLinear‖ * ‖x - y‖

Helper for Theorem 10.46: the displacement of a continuous affine map is controlled by the operator norm of its linear part.

theorem IsSmoothApproximationNonneg.is_l_smooth_on_precompose_continuousAffineMap {E : Type u} {V : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {f : V → ℝ} {φ : E →ᴬ[ℝ] V} {L : NNReal} (hs : is_l_smooth_on f Set.univ L) : is_l_smooth_on (fun (x : E) => f (φ x)) Set.univ (L * ‖φ.contLinear‖₊ ^ 2)

Helper for Theorem 10.46: precomposing a globally smooth function with a continuous affine map multiplies the smoothness constant by the square of the operator norm of the linear part.

theorem IsSmoothApproximationNonneg.nonneg_weighted_sum {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {h1 h1μ h2 h2μ : E → ℝ} {α1 β1 α2 β2 : NNReal} {μ : ↑PosReal} (hh1 : IsSmoothApproximationNonneg h1 h1μ α1 β1 μ) (hh2 : IsSmoothApproximationNonneg h2 h2μ α2 β2 μ) (gamma1 gamma2 : NNReal) : IsSmoothApproximationNonneg (fun (x : E) => ↑gamma1 * h1 x + ↑gamma2 * h2 x) (fun (x : E) => ↑gamma1 * h1μ x + ↑gamma2 * h2μ x) (gamma1 * α1 + gamma2 * α2) (gamma1 * β1 + gamma2 * β2) μ

Theorem 10.46 (1): a nonnegative linear combination of two 1 / μ-smooth approximations is a 1 / μ-smooth approximation of the corresponding nonnegative linear combination, with parameters obtained by the same linear combination.

theorem IsSmoothApproximationNonneg.precompose_continuousAffineMap {E : Type u} {V : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {h hμ : V → ℝ} {α β : NNReal} {μ : ↑PosReal} (hh : IsSmoothApproximationNonneg h hμ α β μ) (φ : E →ᴬ[ℝ] V) : IsSmoothApproximationNonneg (fun (x : E) => h (φ x)) (fun (x : E) => hμ (φ x)) (α * ‖φ.contLinear‖₊ ^ 2) β μ

Theorem 10.46 (2): precomposing a 1 / μ-smooth approximation with a continuous affine map φ multiplies the smoothness parameter by ‖φ.contLinear‖² and leaves the error parameter unchanged.

theorem IsSmoothApproximationNonneg.precompose_linearMap_add {E : Type u} {V : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {h hμ : V → ℝ} {α β : NNReal} {μ : ↑PosReal} (hh : IsSmoothApproximationNonneg h hμ α β μ) (A : E →L[ℝ] V) (b : V) : IsSmoothApproximationNonneg (fun (x : E) => h (A x + b)) (fun (x : E) => hμ (A x + b)) (α * ‖A‖₊ ^ 2) β μ

Source-facing specialization of Theorem 10.46 (2) to affine maps written as x ↦ A x + b.