Global Lipschitzness of a Compactly Supported Cutoff Product

This is the cutoff localization statement labeled S5d.

Let $V$ be a finite-dimensional real normed space, $V'$ a real normed space, and let $\gamma:V\to\mathbb R$ be Lipschitz with a nonnegative Lipschitz constant and compact support. Let $f:V\to V'$ be locally Lipschitz. Then there exist $K\in\mathbb R_{\ge0}$ and $B\in\mathbb R$ such that:

1. the map $x\mapsto\gamma(x)\,f(x)$ is globally Lipschitz with constant $K$;
2. for every $x\in V$,

Scalar multiplication is the given action of $\mathbb R$ on $V'$. The theorem is a compact-localization tool and does not assert a particular formula for either bound.

Original Lean declaration header

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

theorem exists_lipschitzWith_smul_of_locallyLipschitz {γ : V → ℝ} {Kγ : ℝ≥0}
    (hγ : LipschitzWith Kγ γ) (hγs : HasCompactSupport γ) {f : V → V'}
    (hf : LocallyLipschitz f) :
    (∃ K : ℝ≥0, LipschitzWith K fun x => γ x • f x) ∧ ∃ B : ℝ, ∀ x, ‖γ x • f x‖ ≤ B

Module navigation

Module: Analysis/Cutoff/LipschitzBall.

Source excerpt, lines 55–58 · Frozen source 408915f.