Weak Leibniz Rule for Finite Products

This is a weak finite-product Leibniz rule on $\mathbb{R}^n$.

Let $s$ be a finite set of indices, let $f_i$ and $df_i$ be real-valued functions, and let $v$ be a direction. Assume for every $i\in s$ that $f_i$ has weak derivative $df_i$ along $v$, each $f_i$ belongs to $L^{\infty}$ with respect to Lebesgue measure, and each $df_i$ belongs locally to $L^2$ on compact sets. Then the product has weak derivative

and the displayed derivative belongs locally to $L^2$ on every compact set. The assertion includes the empty-product case.

Original Lean declaration header

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

theorem hasWeakDerivAlong_finsetProd_of_locally_memLp_two {n : ℕ} {ι : Type*}
    [DecidableEq ι] (s : Finset ι)
    {f df : ι → EuclideanSpace ℝ (Fin n) → ℝ}
    {v : EuclideanSpace ℝ (Fin n)}
    (hf : ∀ i ∈ s, HasWeakDerivAlong (f i) (df i) v)
    (hbound : ∀ i ∈ s, MemLp (f i) (⊤ : ENNReal)
      (volume : Measure (EuclideanSpace ℝ (Fin n))))
    (hdf2 : ∀ i ∈ s, ∀ S : Set (EuclideanSpace ℝ (Fin n)), IsCompact S →
      MemLp (df i) 2 ((volume : Measure (EuclideanSpace ℝ (Fin n))).restrict S)) :
    HasWeakDerivAlong (fun x => ∏ i ∈ s, f i x)
      (fun x => ∑ i ∈ s, df i x * ∏ j ∈ s.erase i, f j x) v ∧
    ∀ S : Set (EuclideanSpace ℝ (Fin n)), IsCompact S →
      MemLp (fun x => ∑ i ∈ s, df i x * ∏ j ∈ s.erase i, f j x) 2
        ((volume : Measure (EuclideanSpace ℝ (Fin n))).restrict S)

Module navigation

Module: Analysis/WeakDerivative/Calculus.

Definition modules: Analysis/WeakDerivative/Basic.

Supporting theorems: HasWeakDerivAlong.mul_of_locally_memLp_two, hasWeakDerivAlong_of_contDiff.

Previous: hasWeakDerivAlong_finsetSum_mul · Next: hasWeakDerivAlong_exp_neg_of_lipschitz.

Source excerpt, lines 432–445 · Frozen source 408915f.