Documentation

LeanPool.CaffarelliKohnNirenberg.Foundation.Sobolev.Cutoff.Profile

A quantitative smooth transition profile #

This file records the one-dimensional profile used by the ball and space-time cutoff constructions.

Adapted from PDEFoundation (EllipticRegularity, 2026) with the author's permission. The namespace and imports are independent.

Main definitions #

Main results #

source
noncomputable def CKN.smoothTransitionProfile :
ℝ → ℝ

The canonical smooth transition from 0 to 1.

Equations
Instances For
    source
    theorem CKN.smoothTransitionProfile.smooth :
    ContDiff ℝ (↑⊤) smoothTransitionProfile

    The canonical transition profile is smooth to every order.

    source
    theorem CKN.smoothTransitionProfile.zero_of_nonpos {t : ℝ} (ht : t ≤ 0) :
    smoothTransitionProfile t = 0

    The canonical transition profile vanishes to the left of 0.

    source
    theorem CKN.smoothTransitionProfile.one_of_one_le {t : ℝ} (ht : 1 ≤ t) :
    smoothTransitionProfile t = 1

    The canonical transition profile equals 1 to the right of 1.

    source
    theorem CKN.smoothTransitionProfile.nonneg (t : ℝ) :
    0 ≤ smoothTransitionProfile t

    The canonical transition profile is nonnegative.

    source
    theorem CKN.smoothTransitionProfile.le_one (t : ℝ) :
    smoothTransitionProfile t ≤ 1

    The canonical transition profile is at most 1.

    source
    def CKN.smoothTransitionProfile.derivBound :
    ℝ

    The explicit first-derivative constant for the canonical transition.

    Equations
    Instances For
      source
      @[simp]
      theorem CKN.smoothTransitionProfile.derivBound_eq_eight :
      derivBound = 8
      source
      theorem CKN.smoothTransitionProfile.abs_deriv_le_eight (t : ℝ) :
      |deriv smoothTransitionProfile t| ≤ 8

      The absolute value of the first derivative is bounded by 8.