Admissibility Characterized By Function And Gradient $L^2$ Membership

This theorem characterizes the existing local-slope admissibility predicate in finite-dimensional Euclidean space.

Let $E$ be a finite-dimensional complete real inner-product normed space with its Borel measurable structure and second-countable topology. Let $\nu$ be a probability measure on $E$, let $m$ be an additive Haar measure, and assume

For every function $f:E\to\mathbb R$, admissibility with respect to $\nu$ is equivalent to the conjunction of local Lipschitz regularity, square-integrability of $f$, and square-integrability of its gradient:

The Lean declaration is admissible_iff_memLp_gradient_readable. The two $L^2$ conditions are expressed by MemLp with exponent $2$; the conclusion is an iff, not merely an implication. The associated gradient energy may take values in $[0,\infty]$, while the displayed $L^2$ membership condition requires finiteness.

Original Lean declaration header

Within namespace FunctionalInequalities.Energy.LocalSlope. Shown in its original module context. Proof omitted.

theorem admissible_iff_memLp_gradient (hν : (ν : Measure E) ≪ m) (f : E → ℝ) :
    Admissible ν f ↔
      LocallyLipschitz f ∧ MemLp f 2 (ν : Measure E) ∧ MemLp (gradient f) 2 (ν : Measure E)

Module navigation

Module: Energy/LocalSlope/Gradient.

Definition modules: Energy/LocalSlope/Basic.

Supporting theorems: apply_eq_norm_gradient.

Previous: apply_eq_norm_gradient.

Source excerpt, lines 115–117 · Frozen source 408915f.