Monotone Smooth-Transition Exhaustion

Proved

FunctionalInequalities.Analysis.monotoneOn_and_tendsto_smoothTransition_two_sub_div_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readableletwin2026log-concave

This formalizes the scalar exhaustion part of Lemma A.4 of Letwin (arXiv:2607.24164v1), p. 17.

For every $a\in\mathbb R$ , define

\chi_R=\operatorname{smoothTransition}(2-a/R).

As a function of the positive parameter $R$ , $\chi_R$ is monotone on $(0,\infty)$ , and

\lim_{R\to\infty}\operatorname{smoothTransition}(2-a/R)=1.

The limit is expressed as convergence along the real filter atTop to the neighborhood of $1$ .

This is a scalar monotone-exhaustion tool for cutoff constructions.

Original Lean declaration header

Within namespace FunctionalInequalities.Analysis. Shown in its original module context. Proof omitted.

theorem monotoneOn_and_tendsto_smoothTransition_two_sub_div (a : ℝ) :
    MonotoneOn (fun R : ℝ => Real.smoothTransition (2 - a / R)) (Set.Ioi 0) ∧
      Filter.Tendsto (fun R : ℝ => Real.smoothTransition (2 - a / R)) Filter.atTop (nhds 1)

Module navigation

Module: Analysis/Cutoff/Profile.

Previous: deriv_comp_sub_div_and_deriv_deriv.

Source excerpt, lines 422–424 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Cutoff_Profile

Formal statement


theorem FunctionalInequalities.Analysis.monotoneOn_and_tendsto_smoothTransition_two_sub_div_readable (a : ℝ) :
    MonotoneOn (fun R : ℝ => Real.smoothTransition (2 - a / R)) (Set.Ioi 0) ∧
      Filter.Tendsto (fun R : ℝ => Real.smoothTransition (2 - a / R)) Filter.atTop (nhds 1) := by sorry

Source

Source: Letwin, The KLS constant is O(log^(1/4) n) (arXiv:2607.24164v1), Lemma A.4. Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/Cutoff/Profile.lean#L420-L468 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.Cutoff.Profile`, declaration `FunctionalInequalities.Analysis.monotoneOn_and_tendsto_smoothTransition_two_sub_div`; the repository is private at upload time).

View graph