Derivative of a Weighted Coordinate Test

This is a technical coordinate identity for weighted test functions.

Let $n\in\mathbb N$, let $u,a,f:\mathbb R^n\to\mathbb R$ be functions on $\mathrm{EuclideanSpace}\ \mathbb R\ (\mathrm{Fin}\ n)$, with $u$ and $a$ of class $C^1$ and $f$ of class $C^2$. For $i,j\in\mathrm{Fin}\ n$ and $x\in\mathbb R^n$, the $j$-th coordinate derivative of the weighted test weightedTest u a f i is

This lemma supplies a pointwise product-and-chain-rule calculation used by the weak inverse-Hessian integration-by-parts identities.

Original Lean declaration header

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

private lemma smooth_test_derivative {n : ℕ}
    {u a f : EuclideanSpace ℝ (Fin n) → ℝ}
    (hu : ContDiff ℝ 1 u) (ha : ContDiff ℝ 1 a)
    (hf : ContDiff ℝ 2 f) (i j : Fin n)
    (x : EuclideanSpace ℝ (Fin n)) :
    coord (weightedTest u a f i) j x =
      Real.exp (-u x) *
        (coord a j x * coord f i x -
          a x * coord u j x * coord f i x +
          a x * hessianMatrix f x j i)

Module navigation

Module: Analysis/BakryEmery/IntegrationByParts/InverseHessian/Weak.

Definition modules: Analysis/BakryEmery/HessianOperator.

Previous: sum_inv_gradient_test_sub_chain_eq · Next: assemble_generator.

Source excerpt, lines 543–552 · Frozen source 408915f.