OAI/Probability/InvariantIsing/Arrays/TensorSiteComparison.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Covariance changes from varying only the ordinary Gaussian site increments, while the monomial perturbation remains fixed.

  1. lemma OAI.InvariantIsing.tensorLeafCoefficients_profile_cross line 12
  2. lemma OAI.InvariantIsing.tensorSite_increment_cross_le line 35