The derivative of a clamped function

For a continuous real function w and η > 0, Lean's totalized fderiv of the clamped function max 0 (min w η) equals fderiv w on the open band {0 < w < η} and zero everywhere else (TauCeti.fderiv_max_min_eq_indicator). No differentiability of w is assumed: on the band the clamped function agrees with w nearby, and off the closed band it is locally constant. On the two levels 0 and η the clamped function attains a local extremum, so its fderiv is zero there either because it is differentiable with zero derivative or because fderiv is zero by convention at a point of non-differentiability; the identity does not assert differentiability there, and the clamped function is in general not differentiable at those levels.

Clamped functions of this form are the standard test functions for integration by parts against the indicator of a superlevel set. The clamped function differs from η times the indicator of {w > 0} by at most η, and only on the band {0 < w < η} (TauCeti.abs_mul_indicator_sub_max_min_le), for any real function w on any type. Against a real weight d, the error is at most η |d| on the band (TauCeti.norm_mul_sub_clamp_le_indicator).

theorem TauCeti.abs_mul_indicator_sub_max_min_le {X : Type u_1} {w : X → ℝ} {η : ℝ} (hη : 0 ≤ η) (x : X) : |η * {x : X | 0 < w x}.indicator 1 x - max 0 (min (w x) η)| ≤ (w ⁻¹' Set.Ioo 0 η).indicator (fun (x : X) => η) x

The clamped function max 0 (min w η) differs from η times the indicator of {w > 0} by at most η, and only on the band {0 < w < η}.

theorem TauCeti.norm_mul_sub_clamp_le_indicator {X : Type u_1} {w : X → ℝ} {η : ℝ} (hη : 0 ≤ η) (d : ℝ) (x : X) : ‖d * (η * {x : X | 0 < w x}.indicator 1 x - max 0 (min (w x) η))‖ ≤ η * (w ⁻¹' Set.Ioo 0 η).indicator (fun (x : X) => |d|) x

The clamped function max 0 (min w η) agrees with η 1_{w > 0} off the shell {0 < w < η} and differs from it by at most η on the shell; so against any d the error is at most η |d| on the shell and zero off it.

theorem TauCeti.fderiv_max_min_eq_indicator {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {w : E → ℝ} (hw : Continuous w) {η : ℝ} (hη : 0 < η) (x : E) : fderiv ℝ (fun (y : E) => max 0 (min (w y) η)) x = (w ⁻¹' Set.Ioo 0 η).indicator (fderiv ℝ w) x

Lean's totalized fderiv of the clamped function max 0 (min w η) is fderiv w on {0 < w < η} and zero elsewhere. At the levels 0 and η this is an identity for fderiv only: it does not assert that the clamped function is differentiable there, and in general it is not.