Localized Weak Product Data

This is a localized product rule that also supplies support and integrability information. It is listed as a partial formalization of Theorem 2.5 of Letwin (2026).

Let $n\in\mathbb{N}$, let $f,df:\mathrm{EuclideanSpace}\,\mathbb{R}\,(\mathrm{Fin}\,n)\to\mathbb{R}$, and let $v$ be a vector in the same space. Assume:

1. HasWeakDerivAlong f df v.
2. For every compact $S$, $df\in L^2(\operatorname{volume}|_S)$.
3. For every compact $S$, $f\in L^\infty(\operatorname{volume}|_S)$, expressed as MemLp with exponent $\top$.
4. $\psi$ is $C^1$ and compactly supported.

Then HasWeakDerivAlong holds for $\psi f$ with derivative

Moreover, both this product and its displayed weak derivative have compact support, and the derivative belongs globally to $L^2(\operatorname{volume})$. This packages the regularity properties needed for compactly supported testing.

Original Lean declaration header

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

theorem HasWeakDerivAlong.compact_mul_data {n : ℕ}
    {f df : EuclideanSpace ℝ (Fin n) → ℝ} {v : EuclideanSpace ℝ (Fin n)}
    (h : HasWeakDerivAlong f df v)
    (hdf : ∀ S : Set (EuclideanSpace ℝ (Fin n)), IsCompact S →
      MemLp df 2 ((volume : Measure (EuclideanSpace ℝ (Fin n))).restrict S))
    (hf : ∀ S : Set (EuclideanSpace ℝ (Fin n)), IsCompact S →
      MemLp f (⊤ : ENNReal) ((volume : Measure (EuclideanSpace ℝ (Fin n))).restrict S))
    {ψ : EuclideanSpace ℝ (Fin n) → ℝ}
    (hψ : ContDiff ℝ 1 ψ) (hψc : HasCompactSupport ψ) :
    HasWeakDerivAlong (fun x => ψ x * f x)
      (fun x => ψ x * df x + fderiv ℝ ψ x v * f x) v ∧
    HasCompactSupport (fun x => ψ x * f x) ∧
    HasCompactSupport (fun x => ψ x * df x + fderiv ℝ ψ x v * f x) ∧
    MemLp (fun x => ψ x * df x + fderiv ℝ ψ x v * f x) 2
      (volume : Measure (EuclideanSpace ℝ (Fin n)))

Module navigation

Module: Analysis/WeakDerivative/Calculus.

Definition modules: Analysis/WeakDerivative/Basic.

Supporting theorems: HasWeakDerivAlong.mul_contDiff, memLp_mul_of_hasCompactSupport.

Previous: integral_flux_eq_neg_forcing_of_bounded_weak_test · Next: integral_compact_flux_eq_neg_forcing_of_global_bounded_weak_test.

Source excerpt, lines 1355–1369 · Frozen source 408915f.