OAI/Probability/InvariantIsing/Cavity/CavityGaussianBasis.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The finite Gaussian quadratic integral in arbitrary orthonormal coordinates. This is the change-of-basis step for cavity precision.

  1. lemma OAI.InvariantIsing.cavity_basis_reconstruct line 14
  2. lemma OAI.InvariantIsing.cavity_basis_measurable line 21
  3. theorem OAI.InvariantIsing.cavity_gaussian_basis_integrable line 26
  4. theorem OAI.InvariantIsing.cavity_gaussian_basis_integral line 40