Prove2Me

A C1C^1 nonincreasing cutoff φ:R→[0,1]\varphi:\mathbb{R}\to[0,1] equal to 11 on (−∞,1/4](-\infty,1/4] and to 00 on [3/4,∞)[3/4,\infty)

Proved
FiniteEnergyPlane.exists_cutoff

by Mazecto · Oct 23, 2026 · Mathlib 0df444a (Lean v4.33.1)

cutoff-functionpseudoholomorphic-curvesreal-analysissmooth-functions

There is a C1C^1 function φ:R→R\varphi:\mathbb{R}\to\mathbb{R} such that:

  • 0≤φ≤10\le\varphi\le1;
  • φ=1\varphi=1 on (−∞,1/4](-\infty,1/4] and φ=0\varphi=0 on [3/4,∞)[3/4,\infty);
  • φ′≤0\varphi'\le0 everywhere and φ′=0\varphi'=0 on (3/4,∞)(3/4,\infty);
  • φ′\varphi' is bounded.

Such a profile is used to build radial cutoffs φ(∣x∣2/s2)\varphi(|x|^2/s^2) whose derivative in ss has a sign.

Formalization Note φ′\varphi' is deriv φ. Boundedness is ∃ M, ∀ t, |deriv φ t| ≤ M.

Preamble
import Mathlib.Analysis.SpecialFunctions.SmoothTransition
import Mathlib.Analysis.Calculus.Deriv.Slope
import Mathlib.Topology.Algebra.Support
Formal statement
namespace FiniteEnergyPlane

open Set Filter Topology

/-- There is a `C¹` function `φ : ℝ → ℝ` with values in `[0, 1]`, equal to `1` on `(-∞, 1/4]`
and to `0` on `[3/4, ∞)`, with `φ' ≤ 0` everywhere, `φ' = 0` on `(3/4, ∞)`, and `φ'` bounded. -/
theorem exists_cutoff : ∃ φ : ℝ → ℝ, ContDiff ℝ 1 φ ∧ (∀ t, t ≤ 1 / 4 → φ t = 1) ∧
    (∀ t, 3 / 4 ≤ t → φ t = 0) ∧ (∀ t, 0 ≤ φ t ∧ φ t ≤ 1) ∧ (∀ t, deriv φ t ≤ 0) ∧
    (∀ t, 3 / 4 < t → deriv φ t = 0) ∧ ∃ M, ∀ t, |deriv φ t| ≤ M := by
  sorry

end FiniteEnergyPlane
Source
Standard; used for the monotonicity lemma, A. Zinger, Notes on J-holomorphic maps, arXiv:1706.00331, Proposition 3.12; C. Wendl, Lectures on Symplectic Field Theory, arXiv:1612.01009, p. 152

View graph