Smooth Test Approximation In The Lipschitz Graph Domain

This theorem supplies a graph-norm approximating sequence for every smooth test under a local-density hypothesis.

Let $V$ 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, let $m$ be an additive Haar measure, let $D$ be a local density for $(\nu,m)$, and let $f$ be a smooth-gradient test for $\nu$. Then there exists a sequence $(p_j)$ in the domain of the Lipschitz gradient operator such that

in the product topology as $j\to\infty$. Equivalently, the $L^2$ functions and their operator images converge simultaneously.

The declaration is Test.exists_domain_sequence_tendsto_readable. The sequence consists of domain elements, and the gradient representative is placed in $L^2(\nu)$ using toLp; the statement is a convergence assertion rather than an equality at any finite index.

Original Lean declaration header

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

theorem Test.exists_domain_sequence_tendsto (f : Test ν) :
    ∃ p : ℕ → (lipschitzOperator ν m D).domain,
      Tendsto (fun j ↦ (((p j : (lipschitzOperator ν m D).domain) : Lp ℝ 2 (ν : Measure V)),
        lipschitzOperator ν m D (p j))) atTop
        (𝓝 (f.toL2, (Test.memLp_gradient ν f).toLp (gradient f.toFun)))

Module navigation

Module: Energy/SmoothGradient/Core.

Definition modules: Energy/SmoothGradient/Basic.

Supporting theorems: subset_support.

Previous: subset_support · Next: lipschitzRelaxation_le_relaxation.

Source excerpt, lines 181–185 · Frozen source 408915f.