production module

`AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementJacobianAffineSpectrum`

1 named declarations scanned from AutoSamplingTheory/TechnicalLemmas/Measure/DisplacementJacobianAffineSpectrum.lean.

Imports

AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementJacobianEntropy

Imported by

AutoSamplingTheory.TechnicalLemmas.MeasureAutoSamplingTheory.TechnicalLemmas.Measure.DisplacementJacobianMatrixLogDetTests.DisplacementJacobianAffineSpectrum

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

theorem

AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementJacobianAffineSpectrum.affineIdentityMatrix_mulVec_eigenvectorBasis

Partial Not mapped

- Every eigenvector in the canonical Hermitian eigenbasis of a real SPD matrix `A` remains an eigenvector of `(1-t) I + t A`, with eigenvalue `(1-t) + t * lambda_i`. No ordering claim about `Matrix.IsHermitian.eigenvalues` for the affine matrix is made here.

theorem affineIdentityMatrix_mulVec_eigenvectorBasis
    {ι : Type*} [Fintype ι] [DecidableEq ι]
    (A : Matrix ι ι ℝ) (hA : A.PosDef) (t : ℝ) (i : ι) :
    ((1 - t) • (1 : Matrix ι ι ℝ) + t • A) *ᵥ
        ⇑(hA.isHermitian.eigenvectorBasis i) =
      ((1 - t) + t * hA.isHermitian.eigenvalues i) •
        ⇑(hA.isHermitian.eigenvectorBasis i) := by
  rw [Matrix.add_mulVec, Matrix.smul_mulVec, Matrix.smul_mulVec,
    Matrix.one_mulVec, hA.isHermitian.mulVec_eigenvectorBasis]
  simp [smul_smul, add_smul]

end

end DisplacementJacobianAffineSpectrum
end Measure
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/Measure/DisplacementJacobianAffineSpectrum.lean:32published source at 0e31a3cda412