OAI/Geometry/EinsteinFour/ScalarNormalizer.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The positive scalar normalizer used in finite radial compression.

  1. def OAI.PositiveEinsteinFour.Jacobi.scalarNormalizer line 15
  2. theorem OAI.PositiveEinsteinFour.Jacobi.scalarNormalizer_posSemidef line 18
  3. theorem OAI.PositiveEinsteinFour.Jacobi.scalarNormalizer_square line 21
  4. theorem OAI.PositiveEinsteinFour.Jacobi.scalarNormalizer_normalizes line 25
  5. theorem OAI.PositiveEinsteinFour.Jacobi.positive_square_root_eigenvector line 33
  6. theorem OAI.PositiveEinsteinFour.Jacobi.scalarNormalizer_eigenvector line 53

    Source documentation

    The normalizer acts by the reciprocal square root on the prescribed positive scalar eigenmode.

    theorem scalarNormalizer_eigenvector {N : ℕ}
    {L : Matrix (Fin N) (Fin N) ℝ} (hL : L.PosDef)
    {w : Fin N → ℝ} {lam : ℝ} (hlam : 0 < lam) (heigen : L *ᵥ w = lam • w) :
    scalarNormalizer L *ᵥ w = (1 / Real.sqrt lam) • w := by
…

    Mentions: OAI.PositiveEinsteinFour.Jacobi.scalarNormalizer