Clamping Does Not Increase Distance

Proved

LevyStochCalc.Probability.abs_clamp_sub_le_readable

by Lazyfill · Oct 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concavevendored-levystochcalc

This is an elementary estimate for projection onto a time interval.

Let $t\ge0$ , let $s\in[0,t]$ , and let $x\in\mathbb R$ . Then clamping $x$ to $[0,t]$ does not increase its distance from $s$ :

\left|\max\{0,\min\{t,x\}\}-s\right| \le |x-s|.

The estimate is used to control time arguments after localization or truncation.

Original Lean declaration header

Within namespace LevyStochCalc.Probability. Shown in its original module context. Proof omitted.

theorem abs_clamp_sub_le {t : ℝ} (ht : 0 ≤ t) {s : ℝ} (hs : s ∈ Set.Icc (0 : ℝ) t) (x : ℝ) :
    |max 0 (min t x) - s| ≤ |x - s|

Module navigation

Module: LevyStochCalc/Probability/ExitTime.

Previous: exitTime_le_iff · Next: exitTime_le_iff_forall.

Source excerpt, lines 87–88 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_LevyStochCalc_Probability_ExitTime

/-
Copyright (c) 2026 Christian Garry. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Christian Garry
-/
-- Vendored from https://github.com/cgarryZA/LevyStochCalc at commit 984dbf0b790031eac05d56fe5a84b65e15e1e932 (upstream path LevyStochCalc/Probability/ExitTime.lean; Apache-2.0; provenance in formalization/vendor/vendor-lock.json of the KLS repository)
universe u v

Formal statement


theorem LevyStochCalc.Probability.abs_clamp_sub_le_readable {t : ℝ} (ht : 0 ≤ t) {s : ℝ} (hs : s ∈ Set.Icc (0 : ℝ) t) (x : ℝ) :
    |max 0 (min t x) - s| ≤ |x - s| := by sorry

Source

Lean source: https://github.com/cgarryZA/LevyStochCalc/blob/984dbf0b790031eac05d56fe5a84b65e15e1e932/LevyStochCalc/Probability/ExitTime.lean#L86-L99 (repository human-ai-mathematics/kls-lean, commit 408915f, module `LevyStochCalc.Probability.ExitTime`, declaration `LevyStochCalc.Probability.abs_clamp_sub_le`; the repository is private at upload time). Vendored from https://github.com/cgarryZA/LevyStochCalc at commit 984dbf0b790031eac05d56fe5a84b65e15e1e932 (Apache-2.0; upstream copyright notice retained in the Lean text).

View graph