OAI/Probability/SKGap/Localization/PhiHessianBridge.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.SKGapCutoff.Recipe.rank_toEuclideanCLMline 14 - lemma
OAI.SKGapCutoff.Recipe.fieldHessian_matrixline 25 - lemma
OAI.SKGapCutoff.Recipe.onsager_scalarVarianceline 39 - lemma
OAI.SKGapCutoff.Recipe.literal_stableMatrix_eq_hessianline 47 - lemma
OAI.SKGapCutoff.Recipe.literal_stableMatrix_quadraticline 59