Finite Sums Preserve Directional Weak Derivatives

This is a calculus rule for finite linear combinations of directional weak derivatives.

Let $s$ be a finite set of indices, let $c_i\in\mathbb R$, and let $f_i,df_i:\operatorname{EuclideanSpace}(\mathbb R,\operatorname{Fin}(n))\to\mathbb R$. Fix a direction $v$. Assume:

1. For every $i\in s$, df i is the weak derivative of f i along $v$.
2. For every $i\in s$ and every compact set $S$, df i belongs to $L^2(S)$.

Then the finite sum has weak derivative

and the resulting derivative belongs to $L^2(S)$ for every compact $S$. The declaration hasWeakDerivAlong_finsetSum_mul_readable preserves the exact directional weak-derivative relation and compact-local $L^2$ membership.

Original Lean declaration header

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

theorem hasWeakDerivAlong_finsetSum_mul {n : ℕ} {ι : Type*}
    (s : Finset ι) (c : ι → ℝ)
    {f df : ι → EuclideanSpace ℝ (Fin n) → ℝ}
    {v : EuclideanSpace ℝ (Fin n)}
    (hf : ∀ i ∈ s, HasWeakDerivAlong (f i) (df i) v)
    (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, c i * f i x)
      (fun x => ∑ i ∈ s, c i * df i x) v ∧
    ∀ S : Set (EuclideanSpace ℝ (Fin n)), IsCompact S →
      MemLp (fun x => ∑ i ∈ s, c i * df i x) 2
        ((volume : Measure (EuclideanSpace ℝ (Fin n))).restrict S)

Module navigation

Module: Analysis/WeakDerivative/Calculus.

Definition modules: Analysis/WeakDerivative/Basic.

Previous: HasWeakDerivAlong.mul_of_locally_memLp_two · Next: hasWeakDerivAlong_finsetProd_of_locally_memLp_two.

Source excerpt, lines 361–372 · Frozen source 408915f.