Weak Derivatives of a Two-Sided Matrix Product

This gives boundedness and weak derivative data for entries of a constant two-sided matrix product.

Let $d,n\in\mathbb N$, let $S\in M_n(\mathbb R)$ be constant, let $H,DH:\mathbb R^d\to M_n(\mathbb R)$, let $v\in\mathbb R^d$, and let $M\in\mathbb R$. Assume every entry of $H$ has weak derivative given by the corresponding entry of $DH$ in direction $v$, every entry satisfies $\|H_{ab}(x)\|\le M$, and every entry of $DH$ is in $L^2$ on every compact restriction of volume measure.

For every $i,j\in\operatorname{Fin}(n)$, the entry of $SH(x)S$ satisfies

has weak derivative $(SDH(x)S)_{ij}$ in direction $v$, and that derivative belongs to $L^2$ on every compact set. The declaration is bounded_weak_matrix_product_entry_readable and has no positivity, invertibility, or nonzero-dimension assumptions.

Original Lean declaration header

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

theorem bounded_weak_matrix_product_entry {d n : ℕ}
    (S : Matrix (Fin n) (Fin n) ℝ)
    {H DH : EuclideanSpace ℝ (Fin d) → Matrix (Fin n) (Fin n) ℝ}
    {v : EuclideanSpace ℝ (Fin d)} (M : ℝ)
    (hH : ∀ a b, HasWeakDerivAlong (fun x => H x a b) (fun x => DH x a b) v)
    (hbound : ∀ x a b, ‖H x a b‖ ≤ M)
    (hD : ∀ a b, ∀ K : Set (EuclideanSpace ℝ (Fin d)), IsCompact K →
      MemLp (fun x => DH x a b) 2 ((volume : Measure (EuclideanSpace ℝ (Fin d))).restrict K))
    (i j : Fin n) :
    (∀ x, ‖(S * H x * S) i j‖ ≤
      ∑ q : Fin n × Fin n, ‖S i q.1 * S q.2 j‖ * max M 0) ∧
    HasWeakDerivAlong (fun x => (S * H x * S) i j) (fun x => (S * DH x * S) i j) v ∧
    ∀ K : Set (EuclideanSpace ℝ (Fin d)), IsCompact K →
      MemLp (fun x => (S * DH x * S) i j) 2
        ((volume : Measure (EuclideanSpace ℝ (Fin d))).restrict K)

Module navigation

Module: Analysis/Matrix/WeakDerivative.

Definition modules: Analysis/WeakDerivative/Basic.

Supporting theorems: hasWeakDerivAlong_finsetSum_mul.

Previous: bounded_trace_quadratic_weak_derivative_data.

Source excerpt, lines 290–304 · Frozen source 408915f.