Documentation

LeanPool.AnomalousDiffusion.AVenhance.Infra.Cutoff.SmoothStep

Reusable one-dimensional smooth step and plateau cutoffs.

source
@[reducible, inline]
noncomputable abbrev AVenhance.Infra.Cutoff.step :
ℝ → ℝ

The standard smooth transition from zero to one.

Equations
Instances For
    source
    theorem AVenhance.Infra.Cutoff.step_contDiff :
    ContDiff ℝ (↑⊤) step
    source
    theorem AVenhance.Infra.Cutoff.step_nonneg (x : ℝ) :
    0 ≤ step x
    source
    theorem AVenhance.Infra.Cutoff.step_le_one (x : ℝ) :
    step x ≤ 1
    source
    theorem AVenhance.Infra.Cutoff.step_zero_of_nonpos {x : ℝ} (hx : x ≤ 0) :
    step x = 0
    source
    theorem AVenhance.Infra.Cutoff.step_one_of_one_le {x : ℝ} (hx : 1 ≤ x) :
    step x = 1
    source
    theorem AVenhance.Infra.Cutoff.step_one_sub (x : ℝ) :
    step (1 - x) = 1 - step x

    The reflected transition complements the original transition.

    source
    noncomputable def AVenhance.Infra.Cutoff.plateau (left right margin x : ℝ) :
    ℝ

    A smooth cutoff equal to one on [left,right], with transition width margin on both sides, and zero outside [left-margin,right+margin].

    Equations
    Instances For
      source
      theorem AVenhance.Infra.Cutoff.exists_iteratedDeriv_bound {f : ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hcompact : HasCompactSupport f) (N : ℕ) :
      ∃ (C : ℝ), 1 ≤ C ∧ ∀ j ≤ N, ∀ (x : ℝ), |iteratedDeriv j f x| ≤ C

      Smooth compactly supported functions have a uniform bound for every finite collection of scalar iterated derivatives.

      source
      theorem AVenhance.Infra.Cutoff.SmoothStep.step_deriv_compact :
      HasCompactSupport (deriv step)
      source
      theorem AVenhance.Infra.Cutoff.SmoothStep.step_deriv_contDiff :
      ContDiff ℝ (↑⊤) (deriv step)
      source
      theorem AVenhance.Infra.Cutoff.step_iteratedDeriv_bound (N : ℕ) :
      ∃ (C : ℝ), 1 ≤ C ∧ ∀ j ≤ N, ∀ (x : ℝ), |iteratedDeriv j step x| ≤ C

      The smooth step has a finite uniform bound for every finite collection of iterated derivatives. Derivatives of positive order have compact support because the step is constant outside the unit transition interval.