production module

`AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementDerivativeMatrix`

2 named declarations scanned from AutoSamplingTheory/TechnicalLemmas/Measure/DisplacementDerivativeMatrix.lean.

Imports

AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementMapDerivativeMathlib.LinearAlgebra.Matrix.Basis externalMathlib.LinearAlgebra.Determinant external

Imported by

AutoSamplingTheory.TechnicalLemmas.MeasureAutoSamplingTheory.TechnicalLemmas.Measure.DisplacementDerivativeDetPosAutoSamplingTheory.TechnicalLemmas.Measure.DisplacementDerivativeLogDetTests.DisplacementDerivativeMatrix

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

theorem AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementDerivativeMatrix.toMatrix_affineDisplacementDerivative Partial Not mapped

- In any finite basis, the matrix of the displacement derivative is the literal affine matrix `(1-t) I + t A`, where `A` is the matrix of `T'`.

theorem toMatrix_affineDisplacementDerivative
    (b : Module.Basis ι ℝ E) (T' : E →L[ℝ] E) (t : ℝ) :
    LinearMap.toMatrix b b (affineDisplacementDerivative T' t).toLinearMap =
      (1 - t) • (1 : Matrix ι ι ℝ) +
        t • LinearMap.toMatrix b b T'.toLinearMap := by
  ext i j
  by_cases hij : i = j <;>
    simp [affineDisplacementDerivative, LinearMap.toMatrix_apply, Matrix.one_apply, hij]

/-- The determinant used by the Fréchet/change-of-variables layer is exactly
the determinant of the affine matrix in any finite basis. -/

AutoSamplingTheory/TechnicalLemmas/Measure/DisplacementDerivativeMatrix.lean:35published source at 0e31a3cda412

theorem AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementDerivativeMatrix.det_affineDisplacementDerivative_eq_matrix_det Partial Not mapped

- The determinant used by the Fréchet/change-of-variables layer is exactly the determinant of the affine matrix in any finite basis.

theorem det_affineDisplacementDerivative_eq_matrix_det
    (b : Module.Basis ι ℝ E) (T' : E →L[ℝ] E) (t : ℝ) :
    LinearMap.det (affineDisplacementDerivative T' t).toLinearMap =
      Matrix.det
        ((1 - t) • (1 : Matrix ι ι ℝ) +
          t • LinearMap.toMatrix b b T'.toLinearMap) := by
  rw [← LinearMap.det_toMatrix b]
  rw [toMatrix_affineDisplacementDerivative]

end

end DisplacementDerivativeMatrix
end Measure
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/Measure/DisplacementDerivativeMatrix.lean:46published source at 0e31a3cda412