OAI/Probability/InvariantIsing/Cavity/CavityFiniteCascadeGaussianAverage.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Gaussian marking commutes with the finite labeled-cascade representation, including singular covariance matrices.

  1. theorem OAI.InvariantIsing.cavity_finite_cascade_gaussian_average line 14