OAI/Probability/InvariantIsing/Cavity/CavityDeterminantDerivative.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The finite real-matrix Jacobi formula needed for the logarithmic quadratic normalizer in the cavity calculation.

  1. lemma OAI.InvariantIsing.cavity_determinant_derivative_identity line 13
  2. theorem OAI.InvariantIsing.hasDerivAt_cavityDeterminant line 48
  3. theorem OAI.InvariantIsing.hasDerivAt_cavityLogDeterminant line 68
  4. lemma OAI.InvariantIsing.cavity_matrix_entry_derivative line 77
  5. theorem OAI.InvariantIsing.hasDerivAt_cavityQuadraticLogDet line 89

    Source documentation

    The exact root-trace derivative for the normalizer, without a commutation assumption on the covariance derivative and coefficient.

    theorem hasDerivAt_cavityQuadraticLogDet {d : ℕ}
    (K : Matrix (Fin d) (Fin d) ℝ) (H : ℝ → Matrix (Fin d) (Fin d) ℝ)
    (H' : Matrix (Fin d) (Fin d) ℝ) (x : ℝ)
    (hH : HasDerivAt H H' x) (hdet : IsUnit (1 - H x * K).det) :
    HasDerivAt (fun t => Real.log (1 - H t * K).det)
      (-Matrix.trace (H' * cavityBackwardQuadratic K (H x))) x := by
…

    Mentions: OAI.InvariantIsing.cavityBackwardQuadratic