Weak Piola Identity with Lipschitz Test Functions

This is the weak Piola identity for Lipschitz test functions.

Let $n\in\mathbb N$, let $u:\operatorname{EuclideanSpace}(\mathbb R,\operatorname{Fin}(n))\to\mathbb R$ be $C^1$ with Lipschitz gradient, and let $\psi$ be Lipschitz with compact support. For every row index $i<n$,

where $H(x)=\operatorname{hessianMatrix}(u,x)$ and the integral is with respect to Lebesgue measure. The declaration sum_integral_adjugate_hessianMatrix_mul_fderiv_eq_zero_of_lipschitz_readable is a weak, integrated version of the smooth Piola identity. No positivity or invertibility of the Hessian is assumed.

Original Lean declaration header

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

theorem sum_integral_adjugate_hessianMatrix_mul_fderiv_eq_zero_of_lipschitz {n : ℕ}
    {u : EuclideanSpace ℝ (Fin n) → ℝ} (hu : ContDiff ℝ 1 u) {G : NNReal}
    (hG : LipschitzWith G (gradient u)) {ψ : EuclideanSpace ℝ (Fin n) → ℝ} {Lψ : NNReal}
    (hψ : LipschitzWith Lψ ψ) (hψc : HasCompactSupport ψ) (i : Fin n) :
    ∑ j, ∫ x, (hessianMatrix u x).adjugate i j * fderiv ℝ ψ x (EuclideanSpace.basisFun (Fin n) ℝ j)
      ∂(volume : Measure (EuclideanSpace ℝ (Fin n))) = 0

Module navigation

Module: Analysis/Matrix/Piola.

Definition modules: Analysis/BakryEmery/HessianOperator.

Supporting theorems: exists_contDiff_approx_of_lipschitz_gradient, sum_fderiv_adjugate_hessianMatrix_eq_zero.

Previous: sum_fderiv_adjugate_hessianMatrix_eq_zero · Next: sum_integral_inv_hessianMatrix_mul_fderiv_eq.

Source excerpt, lines 822–827 · Frozen source 408915f.