Common-Compact-Support Approximation of Two Weak Derivatives

This formalizes a supporting density component associated with Lemma 2.4 of Letwin (arXiv:2607.24164v1), with a reviewed relation to the cited result.

Let $\eta,a,b:\operatorname{EuclideanSpace}\,\mathbb R\,(\operatorname{Fin}(n))\to\mathbb R$ and let $v,w$ be vectors. Assume:

1. $a$ is a weak derivative of $\eta$ along $v$, and $b$ is a weak derivative of $\eta$ along $w$;
2. $\eta$, $a$, and $b$ have compact support;
3. $a,b\in L^2(\operatorname{vol})$.

Then there exist a compact set $S$ and smooth compactly supported functions $\theta_m$ such that the supports of $\eta,a,b,\theta_m$, and the directional derivatives $D\theta_m(\cdot)v,D\theta_m(\cdot)w$ lie in $S$, while both derivatives belong to $L^2(\operatorname{vol})$ and

The conclusion is a two-direction compact approximation result and does not assert approximation of all coordinate derivatives.

Original Lean declaration header

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

theorem exists_contDiff_compact_weak_deriv_approximation {n : ℕ}
    {η a b : EuclideanSpace ℝ (Fin n) → ℝ} {v w : EuclideanSpace ℝ (Fin n)}
    (hηv : HasWeakDerivAlong η a v) (hηw : HasWeakDerivAlong η b w)
    (hηc : HasCompactSupport η) (hac : HasCompactSupport a) (hbc : HasCompactSupport b)
    (ha2 : MemLp a 2 (volume : Measure (EuclideanSpace ℝ (Fin n))))
    (hb2 : MemLp b 2 (volume : Measure (EuclideanSpace ℝ (Fin n)))) :
    ∃ S : Set (EuclideanSpace ℝ (Fin n)), IsCompact S ∧
      Function.support (η) ⊆ S ∧ Function.support (a) ⊆ S ∧
      Function.support (b) ⊆ S ∧
      ∃ θ : ℕ → EuclideanSpace ℝ (Fin n) → ℝ,
        (∀ m, ContDiff ℝ ∞ (θ m) ∧ HasCompactSupport (θ m) ∧
          Function.support (θ m) ⊆ S ∧
          Function.support (fun x => fderiv ℝ (θ m) x (v)) ⊆ S ∧
          Function.support (fun x => fderiv ℝ (θ m) x (w)) ⊆ S ∧
          MemLp (fun x => fderiv ℝ (θ m) x (v)) 2 (volume : Measure (EuclideanSpace ℝ (Fin n))) ∧
          MemLp (fun x => fderiv ℝ (θ m) x (w)) 2 (volume : Measure (EuclideanSpace ℝ (Fin n)))) ∧
        Tendsto (fun m => eLpNorm (fun x => fderiv ℝ (θ m) x (v) - (a) x)
          2 (volume : Measure (EuclideanSpace ℝ (Fin n)))) atTop (𝓝 0) ∧
        Tendsto (fun m => eLpNorm (fun x => fderiv ℝ (θ m) x (w) - (b) x)
          2 (volume : Measure (EuclideanSpace ℝ (Fin n)))) atTop (𝓝 0)

Module navigation

Module: Analysis/WeakDerivative/Approximation.

Definition modules: Analysis/WeakDerivative/Basic.

Supporting theorems: lintegral_enorm_convolution_sq_le, tendsto_eLpNorm_convolution_sub, fderiv_convolution_eq_of_hasWeakDerivAlong.

Previous: exists_hasWeakDerivAlong_of_forall_cutoff · Next: exists_contDiff_compact_bounded_weak_deriv_approximation_of_support_subset.

Source excerpt, lines 158–177 · Frozen source 408915f.