Smooth one-dimensional and box cutoffs

Definition

KLSModular_LevyStochCalc_Brownian_SmoothCutoff

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

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-contextvendored-levystochcalc

Vendored from the LevyStochCalc library at https://github.com/cgarryZA/LevyStochCalc, commit 984dbf0b790031eac05d56fe5a84b65e15e1e932. smoothCut k t is a smooth transition-based cutoff, equal to $1$ on the intended inner interval and vanishing outside the intended outer interval as specified by the source conventions. boxCut k z multiplies smoothCut k (z i) over all $i:\mathrm{Fin}\,n$ .

Original module imports

import Mathlib.Analysis.SpecialFunctions.SmoothTransition
import Mathlib.Analysis.Calculus.FDeriv.Const
import Mathlib.Analysis.Calculus.ContDiff.Operations
import Mathlib.Topology.UniformSpace.HeineCantor
import Mathlib.Analysis.Normed.Group.Constructions
import Mathlib.Analysis.Normed.Module.FiniteDimension

Original declaration excerpt

Shown in the original module context.

noncomputable def smoothCut (k t : ℝ) : ℝ :=
  Real.smoothTransition ((4 * k ^ 2 - t ^ 2) * 4 / (7 * k ^ 2))

Module navigation

Project result: The KLS conjecture.

Original module · LevyStochCalc.Brownian.SmoothCutoff · Frozen source 408915f.

Definition code

import Mathlib.Analysis.SpecialFunctions.SmoothTransition
import Mathlib.Analysis.Calculus.FDeriv.Const
import Mathlib.Analysis.Calculus.ContDiff.Operations
import Mathlib.Topology.UniformSpace.HeineCantor
import Mathlib.Analysis.Normed.Group.Constructions
import Mathlib.Analysis.Normed.Module.FiniteDimension

/-
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/SmoothCutoff.lean; Apache-2.0; provenance in formalization/vendor/vendor-lock.json of the KLS repository)
namespace LevyStochCalc
open scoped Topology
section OneDim
/-- A smooth one-dimensional cutoff: `1` on `[-3k/2, 3k/2]` and `0` off `(-2k, 2k)`. -/
noncomputable def smoothCut (k t : ℝ) : ℝ :=
  Real.smoothTransition ((4 * k ^ 2 - t ^ 2) * 4 / (7 * k ^ 2))
end OneDim
section Box
variable {n : ℕ}
/-- The product of the one-dimensional cutoffs over the coordinates. -/
noncomputable def boxCut (k : ℝ) (z : Fin n → ℝ) : ℝ := ∏ i, smoothCut k (z i)
end Box
end LevyStochCalc

Source

Lean source: https://github.com/cgarryZA/LevyStochCalc/blob/984dbf0b790031eac05d56fe5a84b65e15e1e932/LevyStochCalc/Brownian/SmoothCutoff.lean#L37-L62 (repository human-ai-mathematics/kls-lean, commit 408915f, module `LevyStochCalc.Brownian.SmoothCutoff`, definition bundle `KLSModular_LevyStochCalc_Brownian_SmoothCutoff`; 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