Lipschitz regularization by inf-convolution

DefinitionInf-convolution with a multiple of the distance#✓fully proved

Let \(X\) be a metric space with metric \(d\), let \(f : X \to [0,\infty]\), and let \(n\) be a natural number. For \(x \in X\),

\[ g_n(x) = \inf\{f(p) + n\,d(x,p) : p \in X\}, \]

the infimum being taken in \([0,\infty]\).

noncomputable def g (f : X → ENNReal) (n : ℕ) (x : X) : ENNReal :=
  sInf (Set.range fun p : X => f p + n * ENNReal.ofReal (dist x p))

Used by 1

Used byThe inf-convolution of a lower semicontinuous function is Lipschitz

TheoremThe inf-convolution of a lower semicontinuous function is Lipschitz#●ready to prove

Let \(X\) be a metric space with metric \(d\), and let \(f : X \to [0,\infty]\) be lower semicontinuous with \(f(p) < \infty\) for at least one \(p \in X\). For a natural number \(n\) and \(x \in X\) let

\[ g_n(x) = \inf\{f(p) + n\,d(x,p) : p \in X\} \in [0,\infty]. \]

Then \(|g_n(x) - g_n(y)| \le n\,d(x,y)\) for every natural number \(n\) (including \(n = 0\)) and all \(x, y \in X\).

Each \(g_n(x)\) is finite, since \(g_n(x) \le f(p) + n\,d(x,p)\) for the point \(p\) with \(f(p) < \infty\), so the difference is one of real numbers.

public theorem_wanted abs_toReal_g_sub_le_mul_dist (f : X → ENNReal) (hf : LowerSemicontinuous f)
    (hp : ∃ p : X, f p < ⊤)
    (n : ℕ) (x y : X) :
    |(g f n x).toReal - (g f n y).toReal| ≤ n * dist x y

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level I (Functional analysis; Nonlinear functional analysis), problem ma_proofbench_l1_36.

Uses 1

Statement usesInf-convolution with a multiple of the distance

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.