OAI/Probability/InvariantIsing/Cavity/CavityFiniteCovariancePath.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The actual finite cascade covariance path and independent Gaussian increments, including zero increments beyond the terminal level.

  1. def OAI.InvariantIsing.cavityFiniteCovariancePath line 18
  2. def OAI.InvariantIsing.cavityFiniteNoiseCovariance line 23
  3. def OAI.InvariantIsing.cavityFiniteRootCovariance line 30
  4. lemma OAI.InvariantIsing.cavityFiniteCovariancePath_posDef line 46
  5. lemma OAI.InvariantIsing.cavityFiniteCovariancePath_symmetric line 51
  6. lemma OAI.InvariantIsing.cavityFiniteNoiseCovariance_delta line 59
  7. lemma OAI.InvariantIsing.cavityFiniteNoiseCovariance_posSemidef line 67
  8. lemma OAI.InvariantIsing.cavityFiniteNoiseCovariance_posDef line 76
  9. lemma OAI.InvariantIsing.cavityFiniteNoiseCovariance_atomless line 85