OAI/Geometry/EinsteinFour/JacobiLogDetSeries.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The finite-dimensional logarithmic determinant series used by the lower radial comparison. It applies to the scalar Green matrix and its three-dimensional curvature perturbation.

  1. theorem OAI.PositiveEinsteinFour.Jacobi.trace_unitary_conjugation line 14
  2. theorem OAI.PositiveEinsteinFour.Jacobi.det_unitary_conjugation line 20
  3. theorem OAI.PositiveEinsteinFour.Jacobi.trace_pow_eq_sum_eigenvalues line 30
  4. theorem OAI.PositiveEinsteinFour.Jacobi.one_sub_eigenvalues_pos line 41
  5. theorem OAI.PositiveEinsteinFour.Jacobi.log_det_one_sub_eq_sum line 62
  6. theorem OAI.PositiveEinsteinFour.Jacobi.hasSum_trace_pow_neg_log_det line 77

    Source documentation

    The full logarithmic determinant is the sum of ordered matrix moments.

    theorem hasSum_trace_pow_neg_log_det {A : Matrix ι ι ℝ}
    (hA : A.PosSemidef) (hI : (1 - A).PosDef) :
    HasSum (fun k : ℕ => (A ^ (k + 1)).trace / (k + 1))
      (-Real.log (1 - A).det) := by
…