Weak Derivative of a Trace Quadratic

This formalizes the weak differentiation rule for a trace quadratic with locally square-integrable derivative data.

Let $d,n\in\mathbb N$, let $B\in M_n(\mathbb R)$ be constant, let $A,DA:\mathbb R^d\to M_n(\mathbb R)$, and let $v\in\mathbb R^d$. Assume:

1. Every entry $A_{ij}$ has weak derivative $(DA)_{ij}$ in direction $v$.
2. Every entry of $A$ belongs to $L^\infty$ with respect to volume measure.
3. For every compact set $S\subseteq\mathbb R^d$, every entry of $DA$ belongs to $L^2(S)$.

Then the function $x\mapsto\operatorname{tr}(BA(x)BA(x))$ has weak derivative in direction $v$ given by

and this derivative belongs to $L^2(S)$ for every compact $S$. The Lean declaration is hasWeakDerivAlong_trace_quadratic_of_locally_memLp_two_readable. It is a technical polynomial chain rule; zero dimensions and arbitrary real constant matrices are allowed.

Original Lean declaration header

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

theorem hasWeakDerivAlong_trace_quadratic_of_locally_memLp_two {d n : ℕ}
    (B : Matrix (Fin n) (Fin n) ℝ)
    {A DA : EuclideanSpace ℝ (Fin d) → Matrix (Fin n) (Fin n) ℝ}
    {v : EuclideanSpace ℝ (Fin d)}
    (hA : ∀ i j, HasWeakDerivAlong (fun x => A x i j) (fun x => DA x i j) v)
    (hbound : ∀ i j, MemLp (fun x => A x i j) (⊤ : ENNReal)
      (volume : Measure (EuclideanSpace ℝ (Fin d))))
    (hDA2 : ∀ i j, ∀ S : Set (EuclideanSpace ℝ (Fin d)), IsCompact S →
      MemLp (fun x => DA x i j) 2
        ((volume : Measure (EuclideanSpace ℝ (Fin d))).restrict S)) :
    HasWeakDerivAlong (fun x => (B * A x * B * A x).trace)
      (fun x => 2 * (B * A x * B * DA x).trace) v ∧
    ∀ S : Set (EuclideanSpace ℝ (Fin d)), IsCompact S →
      MemLp (fun x => 2 * (B * A x * B * DA x).trace) 2
        ((volume : Measure (EuclideanSpace ℝ (Fin d))).restrict S)

Module navigation

Module: Analysis/Matrix/WeakDerivative.

Definition modules: Analysis/WeakDerivative/Basic.

Supporting theorems: HasWeakDerivAlong.mul_of_locally_memLp_two, hasWeakDerivAlong_finsetSum_mul, trace_mul_mul_mul_eq_sum.

Previous: hasWeakDerivAlong_det_of_locally_memLp_two · Next: ae_weak_matrix_inverse_derivative.

Source excerpt, lines 87–101 · Frozen source 408915f.