Smooth Two-Scale Cutoff Profile

This formalizes the scalar part of Lemma A.4 of Letwin (arXiv:2607.24164v1), with a stronger standalone profile statement.

Define $\eta(t)=\operatorname{smoothTransition}(2-t)$. Then $\eta$ is smooth and antitone, satisfies $0\le\eta(t)\le1$, equals $1$ for $t\le1$, and equals $0$ for $t\ge2$. If $t<1$ or $t>2$, then $\eta'(t)=\eta''(t)=0$. Both $\eta'$ and $\eta''$ have compact support, and there exists $B\ge0$ such that

This is reusable scalar cutoff infrastructure; it does not construct the paper’s full generator estimates.

Original Lean declaration header

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

theorem smoothTransition_two_sub_cutoff :
    ContDiff ℝ ∞ (fun s : ℝ => Real.smoothTransition (2 - s)) ∧ Antitone (fun s : ℝ => Real.smoothTransition (2 - s)) ∧
      (∀ t : ℝ, 0 ≤ Real.smoothTransition (2 - t) ∧ Real.smoothTransition (2 - t) ≤ 1) ∧
      (∀ t : ℝ, t ≤ 1 → Real.smoothTransition (2 - t) = 1) ∧
      (∀ t : ℝ, 2 ≤ t → Real.smoothTransition (2 - t) = 0) ∧
      (∀ t : ℝ, t < 1 ∨ 2 < t →
        deriv (fun s : ℝ => Real.smoothTransition (2 - s)) t = 0 ∧ deriv (deriv (fun s : ℝ => Real.smoothTransition (2 - s))) t = 0) ∧
      HasCompactSupport (deriv (fun s : ℝ => Real.smoothTransition (2 - s))) ∧
      HasCompactSupport (deriv (deriv (fun s : ℝ => Real.smoothTransition (2 - s)))) ∧
      ∃ B : ℝ, 0 ≤ B ∧ ∀ t : ℝ,
        |deriv (fun s : ℝ => Real.smoothTransition (2 - s)) t| ≤ B ∧ |deriv (deriv (fun s : ℝ => Real.smoothTransition (2 - s))) t| ≤ B

Module navigation

Module: Analysis/Cutoff/Profile.

Next: exists_majorant_abs_deriv_deriv_smoothTransition_two_sub.

Source excerpt, lines 35–45 · Frozen source 408915f.