Weak Product Rule from Local Essential Boundedness

This is the fully local version of the weak product rule. 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:\mathrm{EuclideanSpace}\,\mathbb{R}\,(\mathrm{Fin}\,n)\to\mathbb{R}$, and let $v$ be a vector. Assume:

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

Then $fg$ has weak derivative

and this derivative belongs to $L^2(\operatorname{volume}|_S)$ for every compact $S$. No global boundedness or classical $C^1$ regularity is assumed.

Original Lean declaration header

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

theorem HasWeakDerivAlong.mul_of_locally_bounded {n : ℕ}
    {f df g dg : EuclideanSpace ℝ (Fin n) → ℝ}
    {v : EuclideanSpace ℝ (Fin n)}
    (hf : HasWeakDerivAlong f df v) (hg : HasWeakDerivAlong g dg v)
    (hf_top : ∀ S : Set (EuclideanSpace ℝ (Fin n)), IsCompact S →
      MemLp f (⊤ : ENNReal) ((volume : Measure (EuclideanSpace ℝ (Fin n))).restrict S))
    (hg_top : ∀ S : Set (EuclideanSpace ℝ (Fin n)), IsCompact S →
      MemLp g (⊤ : ENNReal) ((volume : Measure (EuclideanSpace ℝ (Fin n))).restrict S))
    (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_locally_memLp_two, memLp_mul_of_hasCompactSupport.

Previous: hasWeakDerivAlong_exp_neg_of_lipschitz · Next: integral_weakDeriv_mul_eq_swap.

Source excerpt, lines 671–687 · Frozen source 408915f.