Weak Product Rule with Bounded Factors and Local Derivative Control

This is a localized weak product rule with globally essentially bounded factors. It is listed as a partial formalization of Theorem 2.5 of Letwin (arXiv:2607.24164v1).

Let $n\in\mathbb{N}$, let $f,df,g,dg$ be real-valued functions on $\mathrm{EuclideanSpace}\,\mathbb{R}\,(\mathrm{Fin}\,n)$, and let $v$ be a vector. Assume:

1. $f$ has weak derivative $df$ along $v$, and $g$ has weak derivative $dg$ along $v$.
2. $f$ and $g$ belong to global $L^\infty(\operatorname{volume})$, represented by MemLp exponent $\top$.
3. For every compact $S$, $df,dg\in L^2(\operatorname{volume}|_S)$.

Then the product has weak derivative

and this derivative belongs to $L^2(\operatorname{volume}|_S)$ for every compact $S$. This is a compact-local product theorem.

Original Lean declaration header

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

theorem HasWeakDerivAlong.mul_of_locally_memLp_two {n : ℕ}
    {f df g dg : EuclideanSpace ℝ (Fin n) → ℝ}
    {v : EuclideanSpace ℝ (Fin n)}
    (hf : HasWeakDerivAlong f df v) (hg : HasWeakDerivAlong g dg v)
    (hf_top : MemLp f (⊤ : ENNReal) (volume : Measure (EuclideanSpace ℝ (Fin n))))
    (hg_top : MemLp g (⊤ : ENNReal) (volume : Measure (EuclideanSpace ℝ (Fin n))))
    (hdf2 : ∀ S : Set (EuclideanSpace ℝ (Fin n)), IsCompact S →
      MemLp df 2 ((volume : Measure (EuclideanSpace ℝ (Fin n))).restrict S))
    (hdg2 : ∀ S : Set (EuclideanSpace ℝ (Fin n)), IsCompact S →
      MemLp dg 2 ((volume : Measure (EuclideanSpace ℝ (Fin n))).restrict S)) :
    HasWeakDerivAlong (fun x => f x * g x)
      (fun x => df x * g x + f x * dg x) v ∧
    ∀ S : Set (EuclideanSpace ℝ (Fin n)), IsCompact S →
      MemLp (fun x => df x * g x + f x * dg x) 2
        ((volume : Measure (EuclideanSpace ℝ (Fin n))).restrict S)

Module navigation

Module: Analysis/WeakDerivative/Calculus.

Definition modules: Analysis/WeakDerivative/Basic.

Supporting theorems: HasWeakDerivAlong.mul_contDiff, HasWeakDerivAlong.mul_of_memLp_two, memLp_mul_of_hasCompactSupport.

Previous: memLp_mul_of_hasCompactSupport · Next: hasWeakDerivAlong_finsetSum_mul.

Source excerpt, lines 211–225 · Frozen source 408915f.