OAI/Probability/InvariantIsing/Cavity/CavityResolventDerivative.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.InvariantIsing.hasDerivAt_cavityMatrixInverse line 15
2. lemma OAI.InvariantIsing.cavityResolvent_identity_add line 29
3. theorem OAI.InvariantIsing.hasDerivAt_cavityResolvent line 48

   Source documentation

   The root covariance identity cav:q-root-covariance holds without commuting the covariance path with the quadratic coefficient.

   theorem hasDerivAt_cavityResolvent {d : ℕ}
       (K : Matrix (Fin d) (Fin d) ℝ) (H : ℝ → Matrix (Fin d) (Fin d) ℝ)
       (H' : Matrix (Fin d) (Fin d) ℝ) (x : ℝ)
       (hK : K.transpose = K) (hHx : (H x).transpose = H x)
       (hH : HasDerivAt H H' x) (hdet : IsUnit (1 - H x * K).det) :
       HasDerivAt (fun t => cavityResolvent K (H t))
         ((1 - H x * K)⁻¹ * H' * ((1 - H x * K)⁻¹).transpose) x := by
   …

   Mentions: OAI.InvariantIsing.cavityResolvent

4. theorem OAI.InvariantIsing.cavity_projected_root_covariance line 70

   Source documentation

   Differentiating the scalar Schur field identifies the projected common-root covariance. The local scalar identity is supplied by the proved finite spectral Schur evaluation.

   theorem cavity_projected_root_covariance {d n : ℕ}
       (K : Matrix (Fin d) (Fin d) ℝ) (H : ℝ → Matrix (Fin d) (Fin d) ℝ)
       (H' : Matrix (Fin d) (Fin d) ℝ) (L : Matrix (Fin d) (Fin n) ℝ)
       (C₀ : Matrix (Fin n) (Fin n) ℝ) (R : ℝ → ℝ) (R' x : ℝ)
       (hK : K.transpose = K) (hHx : (H x).transpose = H x)
       (hH : HasDerivAt H H' x) (hdet : IsUnit (1 - H x * K).det)
       (hR : HasDerivAt R R' x)
       (hscalar : (fun t => C₀ + L.transpose * cavityResolvent K (H t) * L) =ᶠ[𝓝 x]
         (fun t => R t • (1 : Matrix (Fin n) (Fin n) ℝ))) :
       L.transpose * ((1 - H x * K)⁻¹ * H' * ((1 - H x * K)⁻¹).transpose) * L =
         R' • 1 := by
   …

   Mentions: OAI.InvariantIsing.cavityResolvent