Prove2Me

Smooth Compact Majorant for the Cutoff Curvature

Proved
FunctionalInequalities.Analysis.exists_majorant_abs_deriv_deriv_smoothTransition_two_sub_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readableletwin2026log-concave

This formalizes a scalar component of Lemma A.4 of Letwin (arXiv:2607.24164v1).

For η(t)=smoothTransition⁡(2−t)\eta(t)=\operatorname{smoothTransition}(2-t), there exists a smooth compactly supported function w:R→Rw:\mathbb R\to\mathbb R such that w≥0w\ge0, w(t)=0w(t)=0 whenever t≤0t\le0 or 3≤t3\le t, and

∣η′′(t)∣≤w(t)(t∈R).|\eta''(t)|\le w(t)\qquad(t\in\mathbb R).

The function ww is a technical compact majorant for the second derivative of the scalar cutoff.

Original Lean declaration header

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

theorem exists_majorant_abs_deriv_deriv_smoothTransition_two_sub :
    ∃ w : ℝ → ℝ, ContDiff ℝ ∞ w ∧ HasCompactSupport w ∧ (∀ t, 0 ≤ w t) ∧
      (∀ t, t ≤ 0 ∨ 3 ≤ t → w t = 0) ∧
      ∀ t, |deriv (deriv (fun s : ℝ => Real.smoothTransition (2 - s))) t| ≤ w t

Module navigation

Module: Analysis/Cutoff/Profile.

Supporting theorems: smoothTransition_two_sub_cutoff.

Previous: smoothTransition_two_sub_cutoff · Next: inv_mul_intervalIntegral_div_three_cutoff.

Source excerpt, lines 126–129 · Frozen source 408915f.

Preamble
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Cutoff_Profile

open scoped ContDiff
Formal statement

theorem FunctionalInequalities.Analysis.exists_majorant_abs_deriv_deriv_smoothTransition_two_sub_readable :
    ∃ w : ℝ → ℝ, ContDiff ℝ ∞ w ∧ HasCompactSupport w ∧ (∀ t, 0 ≤ w t) ∧
      (∀ t, t ≤ 0 ∨ 3 ≤ t → w t = 0) ∧
      ∀ t, |deriv (deriv (fun s : ℝ => Real.smoothTransition (2 - s))) t| ≤ w t := 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#L124-L192 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.Cutoff.Profile`, declaration `FunctionalInequalities.Analysis.exists_majorant_abs_deriv_deriv_smoothTransition_two_sub`; the repository is private at upload time).

View graph