Real clamp and its basic properties

import Definitions.Def_KLSModular_LevyStochCalc_Brownian_VectorItoVersionExists
import Definitions.Def_KLSModular_LevyStochCalc_Brownian_ItoLinear

/-
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/Brownian/ItoTruncate.lean; Apache-2.0; provenance in formalization/vendor/vendor-lock.json of the KLS repository)
namespace LevyStochCalc
open MeasureTheory
open scoped NNReal ENNReal Topology
section Clamp
/-- The clamp of a real number to `[-j, j]`. -/
noncomputable def clampAt (j x : ℝ) : ℝ := max (-j) (min j x)
theorem clampAt_zero {j : ℝ} (hj : 0 ≤ j) : clampAt j 0 = 0 := by
  unfold clampAt
  rw [min_eq_right hj, max_eq_right (by linarith : -j ≤ (0 : ℝ))]
theorem continuous_clampAt (j : ℝ) : Continuous (clampAt j) := by
  unfold clampAt
  fun_prop
theorem abs_clampAt_le {j : ℝ} (hj : 0 ≤ j) (x : ℝ) : |clampAt j x| ≤ j := by
  unfold clampAt
  rcases le_or_gt x (-j) with hx | hx
  · rw [min_eq_right (by linarith : x ≤ j), max_eq_left hx, abs_neg, abs_of_nonneg hj]
  · rcases le_or_gt x j with hx' | hx'
    · rw [min_eq_right hx', max_eq_right hx.le, abs_le]
      exact ⟨hx.le, hx'⟩
    · rw [min_eq_left hx'.le, max_eq_right (by linarith : -j ≤ j), abs_of_nonneg hj]
end Clamp
end LevyStochCalc