production module

`AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementDerivativeDetPos`

6 named declarations scanned from AutoSamplingTheory/TechnicalLemmas/Measure/DisplacementDerivativeDetPos.lean.

Imports

AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementDerivativeMatrixAutoSamplingTheory.TechnicalLemmas.Measure.DisplacementJacobianEntropyMathlib.Analysis.Matrix.PosDef external

Imported by

AutoSamplingTheory.TechnicalLemmas.MeasureAutoSamplingTheory.TechnicalLemmas.Measure.DisplacementChangeOfVariablesTests.DisplacementDerivativeDetPos

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

theorem AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementDerivativeDetPos.toMatrix_affineDisplacementDerivative_posDef Partial Not mapped

- An SPD matrix representation of the endpoint derivative gives an SPD matrix representation of the affine displacement derivative on the full segment.

theorem toMatrix_affineDisplacementDerivative_posDef
    (b : Module.Basis ι ℝ E) (T' : E →L[ℝ] E)
    (hT : (LinearMap.toMatrix b b T'.toLinearMap).PosDef)
    (t : ℝ) (ht0 : 0 ≤ t) (ht1 : t ≤ 1) :
    (LinearMap.toMatrix b b
      (affineDisplacementDerivative T' t).toLinearMap).PosDef := by
  rw [toMatrix_affineDisplacementDerivative]
  exact affineIdentityMatrix_posDef
    (LinearMap.toMatrix b b T'.toLinearMap) hT t ht0 ht1

/-- A PSD endpoint derivative is already enough for strict positivity of the
interior affine derivative matrix. -/

AutoSamplingTheory/TechnicalLemmas/Measure/DisplacementDerivativeDetPos.lean:39published source at 0e31a3cda412

theorem

AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementDerivativeDetPos.toMatrix_affineDisplacementDerivative_posDef_of_posSemidef

Partial Not mapped

- A PSD endpoint derivative is already enough for strict positivity of the interior affine derivative matrix.

theorem toMatrix_affineDisplacementDerivative_posDef_of_posSemidef
    (b : Module.Basis ι ℝ E) (T' : E →L[ℝ] E)
    (hT : (LinearMap.toMatrix b b T'.toLinearMap).PosSemidef)
    (t : ℝ) (ht0 : 0 ≤ t) (ht1 : t < 1) :
    (LinearMap.toMatrix b b
      (affineDisplacementDerivative T' t).toLinearMap).PosDef := by
  rw [toMatrix_affineDisplacementDerivative]
  exact affineIdentityMatrix_posDef_of_posSemidef
    (LinearMap.toMatrix b b T'.toLinearMap) hT t ht0 ht1

/-- Under an SPD endpoint derivative, the continuous-linear determinant of the
affine displacement derivative is strictly positive. -/

AutoSamplingTheory/TechnicalLemmas/Measure/DisplacementDerivativeDetPos.lean:51published source at 0e31a3cda412

theorem AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementDerivativeDetPos.det_affineDisplacementDerivative_pos Partial Not mapped

- Under an SPD endpoint derivative, the continuous-linear determinant of the affine displacement derivative is strictly positive.

theorem det_affineDisplacementDerivative_pos
    (b : Module.Basis ι ℝ E) (T' : E →L[ℝ] E)
    (hT : (LinearMap.toMatrix b b T'.toLinearMap).PosDef)
    (t : ℝ) (ht0 : 0 ≤ t) (ht1 : t ≤ 1) :
    0 < LinearMap.det (affineDisplacementDerivative T' t).toLinearMap := by
  rw [det_affineDisplacementDerivative_eq_matrix_det b T' t]
  exact (affineIdentityMatrix_posDef
    (LinearMap.toMatrix b b T'.toLinearMap) hT t ht0 ht1).det_pos

/-- Interior-time determinant positivity from the weaker PSD endpoint
hypothesis. -/

AutoSamplingTheory/TechnicalLemmas/Measure/DisplacementDerivativeDetPos.lean:63published source at 0e31a3cda412

theorem

AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementDerivativeDetPos.det_affineDisplacementDerivative_pos_of_posSemidef

Partial Not mapped

- Interior-time determinant positivity from the weaker PSD endpoint hypothesis.

theorem det_affineDisplacementDerivative_pos_of_posSemidef
    (b : Module.Basis ι ℝ E) (T' : E →L[ℝ] E)
    (hT : (LinearMap.toMatrix b b T'.toLinearMap).PosSemidef)
    (t : ℝ) (ht0 : 0 ≤ t) (ht1 : t < 1) :
    0 < LinearMap.det (affineDisplacementDerivative T' t).toLinearMap := by
  rw [det_affineDisplacementDerivative_eq_matrix_det b T' t]
  exact (affineIdentityMatrix_posDef_of_posSemidef
    (LinearMap.toMatrix b b T'.toLinearMap) hT t ht0 ht1).det_pos

/-- The absolute determinant in change of variables is redundant under an SPD
endpoint derivative. -/

AutoSamplingTheory/TechnicalLemmas/Measure/DisplacementDerivativeDetPos.lean:74published source at 0e31a3cda412

theorem AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementDerivativeDetPos.abs_det_affineDisplacementDerivative_eq Partial Not mapped

- The absolute determinant in change of variables is redundant under an SPD endpoint derivative.

theorem abs_det_affineDisplacementDerivative_eq
    (b : Module.Basis ι ℝ E) (T' : E →L[ℝ] E)
    (hT : (LinearMap.toMatrix b b T'.toLinearMap).PosDef)
    (t : ℝ) (ht0 : 0 ≤ t) (ht1 : t ≤ 1) :
    |LinearMap.det (affineDisplacementDerivative T' t).toLinearMap| =
      LinearMap.det (affineDisplacementDerivative T' t).toLinearMap :=
  abs_of_pos (det_affineDisplacementDerivative_pos b T' hT t ht0 ht1)

/-- Interior-time absolute-determinant removal from a PSD endpoint derivative. -/

AutoSamplingTheory/TechnicalLemmas/Measure/DisplacementDerivativeDetPos.lean:85published source at 0e31a3cda412

theorem

AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementDerivativeDetPos.abs_det_affineDisplacementDerivative_eq_of_posSemidef

Partial Not mapped

- Interior-time absolute-determinant removal from a PSD endpoint derivative.

theorem abs_det_affineDisplacementDerivative_eq_of_posSemidef
    (b : Module.Basis ι ℝ E) (T' : E →L[ℝ] E)
    (hT : (LinearMap.toMatrix b b T'.toLinearMap).PosSemidef)
    (t : ℝ) (ht0 : 0 ≤ t) (ht1 : t < 1) :
    |LinearMap.det (affineDisplacementDerivative T' t).toLinearMap| =
      LinearMap.det (affineDisplacementDerivative T' t).toLinearMap :=
  abs_of_pos
    (det_affineDisplacementDerivative_pos_of_posSemidef b T' hT t ht0 ht1)

end

end DisplacementDerivativeDetPos
end Measure
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/Measure/DisplacementDerivativeDetPos.lean:94published source at 0e31a3cda412