Gluing Local Weak Derivatives From Compact Cutoffs

This is a generic gluing theorem for weak derivatives.

Let $E$ be a finite-dimensional real inner-product normed space with its Borel measurable structure, and let $f:E\to\mathbb R$. Assume:

1. for every compact set $S$, the restriction of $f$ to $S$ belongs to $L^2$ with respect to restricted volume;
2. for every $C^1$ compactly supported cutoff $\chi$, there is a globally $L^2$ function $g_\chi$ such that $\chi f$ has weak derivative $g_\chi$ along a fixed vector $v$.

Then there exists $g:E\to\mathbb R$ such that $g$ is a weak derivative of $f$ along $v$, and for every compact $S$, $g$ belongs to $L^2$ with respect to volume restricted to $S$.

The conclusion is local $L^2$ regularity of the derivative rather than global $L^2$ regularity. It provides a cutoff-gluing interface for weak derivative constructions.

Original Lean declaration header

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

theorem exists_hasWeakDerivAlong_of_forall_cutoff {E : Type*} [NormedAddCommGroup E]
    [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    {f : E → ℝ} (hf : ∀ S : Set E, IsCompact S → MemLp f 2 ((volume : Measure E).restrict S)) (v : E)
    (hloc : ∀ χ : E → ℝ, ContDiff ℝ 1 χ → HasCompactSupport χ →
      ∃ g : E → ℝ, HasWeakDerivAlong (fun x => χ x * f x) g v ∧ MemLp g 2 (volume : Measure E)) :
    ∃ g : E → ℝ, HasWeakDerivAlong f g v ∧
      ∀ S : Set E, IsCompact S → MemLp g 2 ((volume : Measure E).restrict S)

Module navigation

Module: Analysis/WeakDerivative/Approximation.

Definition modules: Analysis/WeakDerivative/Basic.

Supporting theorems: HasWeakDerivAlong.mul_contDiff.

Next: exists_contDiff_compact_weak_deriv_approximation.

Source excerpt, lines 27–33 · Frozen source 408915f.