Derivative of a Determinant with One Updated Row

This lemma is a technical determinant differentiation formula.

Let $E$ be a real normed vector space, let $A:E\to\operatorname{Fin}(n)\to\operatorname{Fin}(n)\to\mathbb R$, and suppose every scalar entry $y\mapsto A(y)_{kl}$ is differentiable at $x\in E$. Fix a row $j$, a replacement row $c:\operatorname{Fin}(n)\to\mathbb R$, and a direction $v\in E$. Then

The declaration fderiv_det_updateRow_readable is used as a local algebraic rule and makes no symmetry, positivity, or invertibility assumption on the matrices.

Original Lean declaration header

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

private lemma fderiv_det_updateRow
    {n : ℕ} {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    (A : E → Fin n → Fin n → ℝ) (x : E)
    (hA : ∀ k l, DifferentiableAt ℝ (fun y => A y k l) x)
    (j : Fin n) (c : Fin n → ℝ) (v : E) :
    fderiv ℝ (fun y => (Matrix.updateRow (A y) j c).det) x v =
      ∑ k, if k = j then 0
        else ((Matrix.updateRow (A x) j c).updateRow k
          (fun l => fderiv ℝ (fun y => A y k l) x v)).det

Module navigation

Module: Analysis/Matrix/Piola.

Next: sum_fderiv_adjugate_hessianMatrix_eq_zero.

Source excerpt, lines 57–65 · Frozen source 408915f.