Weak Derivative From an L2 Difference Bound

This formalizes the difference-quotient criterion associated with Nirenberg and Evans, PDE §5.8.2, Theorem 3(ii).

Let $E$ be a finite-dimensional real inner-product normed space, let $f\in L^2(\operatorname{vol})$, and fix $v\in E$. Suppose there is $C\in\mathbb R$ such that for every nonzero $t\in\mathbb R$ with $|t|\le1$,

Then there exists $g\in L^2(\operatorname{vol})$ such that $g$ is a weak derivative of $f$ along $v$.

The theorem is an $L^2$ existence criterion; it does not identify the derivative uniquely by an explicit pointwise formula.

Original Lean declaration header

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

theorem exists_hasWeakDerivAlong_of_sq_difference_le
    {f : E → ℝ} (hf : MemLp f 2 (volume : Measure E)) (v : E) {C : ℝ}
    (hdiff : ∀ t : ℝ, t ≠ 0 → |t| ≤ 1 →
      ∫ x, (f (x + t • v) - f x) ^ 2 ∂(volume : Measure E) ≤ C * t ^ 2) :
    ∃ g : E → ℝ, HasWeakDerivAlong f g v ∧ MemLp g 2 (volume : Measure E)

Module navigation

Module: Analysis/WeakDerivative/Mollification.

Definition modules: Analysis/WeakDerivative/Basic.

Supporting theorems: quotient_pairing_tendsto.

Previous: quotient_pairing_tendsto.

Source excerpt, lines 189–193 · Frozen source 408915f.