noncomputable def absolute_value_log_sum_exp_smoothing (μ : ↑PosReal) : ℝ → ℝ

The two-term shifted log-sum-exp smoothing x ↦ μ log (e^{x / μ} + e^{-x / μ}) - μ log 2 of the absolute value.

@[simp]

theorem absolute_value_log_sum_exp_smoothing_apply (μ : ↑PosReal) (x : ℝ) : absolute_value_log_sum_exp_smoothing μ x = ↑μ * Real.log (Real.exp (x / ↑μ) + Real.exp (-x / ↑μ)) - ↑μ * Real.log 2

Evaluating absolute_value_log_sum_exp_smoothing μ at x gives the shifted two-term log-sum-exp formula from Example 10.50.

theorem coordinatewiseMax_pair_eq_abs (x : ℝ) : coordinatewiseMax !₂[x, -x].ofLp = |x|

Helper for Example 10.50: the coordinatewise maximum of the pair (x, -x) is |x|.

theorem absolute_value_log_sum_exp_smoothing_eq_mul_log_cosh (μ : ↑PosReal) (x : ℝ) : absolute_value_log_sum_exp_smoothing μ x = ↑μ * Real.log (Real.cosh (x / ↑μ))

Helper for Example 10.50: the scalar smoothing rewrites as μ log(cosh (x / μ)).

theorem absolute_value_log_sum_exp_smoothing_hasDerivAt (μ : ↑PosReal) (x : ℝ) : HasDerivAt (absolute_value_log_sum_exp_smoothing μ) (Real.tanh (x / ↑μ)) x

Helper for Example 10.50: the derivative of the scalar smoothing is tanh (x / μ).

theorem absolute_value_log_sum_exp_smoothing_deriv_eq (μ : ↑PosReal) (x : ℝ) : deriv (absolute_value_log_sum_exp_smoothing μ) x = Real.tanh (x / ↑μ)

Helper for Example 10.50: the derivative formula is the pointwise derivative of the smoothing.

theorem absolute_value_log_sum_exp_smoothing_deriv_hasDerivAt (μ : ↑PosReal) (x : ℝ) : HasDerivAt (deriv (absolute_value_log_sum_exp_smoothing μ)) ((↑μ)⁻¹ / Real.cosh (x / ↑μ) ^ 2) x

Helper for Example 10.50: the derivative field itself has derivative μ⁻¹ / cosh(x / μ)^2.

theorem absolute_value_log_sum_exp_smoothing_second_deriv_eq (μ : ↑PosReal) (x : ℝ) : deriv (deriv (absolute_value_log_sum_exp_smoothing μ)) x = (↑μ)⁻¹ / Real.cosh (x / ↑μ) ^ 2

Helper for Example 10.50: the second derivative is μ⁻¹ / cosh(x / μ)^2.

theorem lipschitzWith_deriv_of_is_l_smooth_on_real {f : ℝ → ℝ} {L : NNReal} (hs : is_l_smooth_on f Set.univ L) : LipschitzWith L (deriv f)

Helper for Example 10.50: on the real line, an L-smooth function has an L-Lipschitz ordinary derivative.

theorem is_l_smooth_on_of_lipschitzWith_deriv_real {f : ℝ → ℝ} {L : NNReal} (hdiff : Differentiable ℝ f) (hlip : LipschitzWith L (deriv f)) : is_l_smooth_on f Set.univ L

Helper for Example 10.50: if the derivative is L-Lipschitz on ℝ, then the original function is L-smooth in the Chapter 5 sense.

theorem pair_linear_map_linear_map_add (x y : ℝ) : !₂[x + y, -(x + y)] = !₂[x, -x] + !₂[y, -y]

Helper for Example 10.50: the affine pair map x ↦ (x, -x) as a linear map into ℝ².

theorem pair_linear_map_linear_map_smul (c x : ℝ) : !₂[c * x, -(c * x)] = c • !₂[x, -x]

Helper for Example 10.50: the pair map is homogeneous.

theorem pair_linear_map_norm_sq (x : ℝ) : ‖!₂[x, -x]‖ ^ 2 = 2 * x ^ 2

Helper for Example 10.50: the squared norm of the pair map is 2 x².

theorem pair_linear_map_bound (x : ℝ) : ‖!₂[x, -x]‖ ≤ √2 * ‖x‖

Helper for Example 10.50: the pair map is bounded by √2.

def pair_linear_map_linear : ℝ →ₗ[ℝ] EuclideanSpace ℝ (Fin 2)

Helper for Example 10.50: the linear part of the affine pair map.

noncomputable def pair_linear_map : ℝ →L[ℝ] EuclideanSpace ℝ (Fin 2)

Helper for Example 10.50: the continuous linear pair map x ↦ (x, -x).

@[simp]

theorem pair_linear_map_apply (x : ℝ) : pair_linear_map x = !₂[x, -x]

Helper for Example 10.50: evaluating the continuous pair map recovers (x, -x).

theorem pair_linear_opNorm_sq : ‖pair_linear_map‖₊ ^ 2 = 2

Helper for Example 10.50: the pair map has operator norm squared equal to 2.

theorem absolute_value_log_sum_exp_smoothing_has_loose_nonneg_bound (μ : ↑PosReal) : IsSmoothApproximationNonneg abs (absolute_value_log_sum_exp_smoothing μ) 2 (log_cardinality_nonneg ⋯) μ

Helper for Example 10.50: Theorem 10.46 applied to the pair map yields the looser nonnegative pair (2, log 2).

theorem absolute_value_log_sum_exp_smoothing_has_exact_nonneg_bound (μ : ↑PosReal) : IsSmoothApproximationNonneg abs (absolute_value_log_sum_exp_smoothing μ) 1 (log_cardinality_nonneg ⋯) μ

Helper for Example 10.50: the direct one-dimensional second-derivative computation improves the loose affine-precomposition bound to the exact nonnegative pair (1, log 2).

theorem absolute_value_log_sum_exp_beta_lower_at_scale {μ α β : ↑PosReal} (happrox : IsSmoothApproximation abs (absolute_value_log_sum_exp_smoothing μ) α β μ) {t : ℝ} (ht : 0 ≤ t) : Real.log 2 - Real.log (1 + Real.exp (-2 * t)) ≤ ↑β

Helper for Example 10.50: every admissible error parameter dominates the exact scaled gap at the nonnegative point x = μ t.

theorem absolute_value_log_sum_exp_smoothing_is_smooth_approximation (μ : ↑PosReal) : IsSmoothApproximation abs (absolute_value_log_sum_exp_smoothing μ) 1 (log_cardinality_posreal ⋯) μ

Example 10.50 (1): the shifted two-term log-sum-exp smoothing of |x| is a 1 / μ-smooth approximation with parameters (1, log 2), encoded by the canonical chapter owner log_cardinality_posreal at n = 2.

theorem absolute_value_log_sum_exp_smoothing_parameter_lower_bounds (μ α β : ↑PosReal) (happrox : IsSmoothApproximation abs (absolute_value_log_sum_exp_smoothing μ) α β μ) : 1 ≤ ↑α ∧ Real.log 2 ≤ ↑β

Example 10.50 (2): any positive parameter pair yielding this same chapter-level smooth approximation must satisfy α ≥ 1 and β ≥ log 2.

theorem absolute_value_log_sum_exp_smoothing_has_loose_two_log_two_bound (μ : ↑PosReal) : IsSmoothApproximationNonneg abs (absolute_value_log_sum_exp_smoothing μ) 2 (log_cardinality_nonneg ⋯) μ

The affine-precomposition bound from Theorem 10.46(b) yields the looser nonnegative parameter pair (2, log 2), encoded by log_cardinality_nonneg at n = 2, for the same smoothing family.