OAI/Probability/FreeIsing/Posterior/Smooth.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Problem367.FinitePosterior.contDiff_fieldEnergyline 15 - theorem
OAI.Problem367.FinitePosterior.contDiff_fieldPartitionline 20 - theorem
OAI.Problem367.FinitePosterior.contDiff_fieldMean_allline 26 - theorem
OAI.Problem367.FinitePosterior.contDiff_fieldMassline 37 - theorem
OAI.Problem367.FinitePosterior.fderiv_fieldMean_applyline 42