Continuous Multilinear Determinant Map

For a finite index type $ι$ with decidable equality, detML is the continuous multilinear map over $ℝ$ that takes a family of row vectors, equivalently a matrix $M : ι \to ι \to ℝ$, to its determinant. Its domain is the multilinear product of one copy of $ι \to ℝ$ for each row, and its codomain is $ℝ$. This bundle contains the determinant map used as a foundational object for later derivative and log-determinant formulas; it does not itself state such a derivative formula.

Original module imports

import Mathlib.Analysis.Calculus.FDeriv.Analytic
import Mathlib.Topology.Algebra.Group.Matrix
import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
import Mathlib.LinearAlgebra.Matrix.Trace
import Mathlib.Analysis.Matrix.Normed
import Mathlib.Analysis.SpecialFunctions.Log.Deriv
import Mathlib.Analysis.Calculus.TaylorIntegral
import Mathlib.Analysis.Matrix.PosDef

Original declaration excerpt

Shown in the original module context.

private def detML : ContinuousMultilinearMap ℝ (fun _ : ι => ι → ℝ) ℝ :=
  { (Matrix.detRowAlternating : (ι → ℝ) [⋀^ι]→ₗ[ℝ] ℝ).toMultilinearMap with
    cont := by
      change Continuous (fun M : ι → ι → ℝ => (Matrix.of M).det)
      simp only [Matrix.det_apply, Matrix.of_apply]
      fun_prop }

Module navigation

Theorems in source order:

• fderiv_det_eq_det_mul_trace

Project result: The KLS conjecture.

Original module · FunctionalInequalities.Analysis.Matrix.DeterminantDerivative · Frozen source 408915f.