OAI/Probability/InvariantIsing/Fields/VectorTerminalCascade.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Ancestor kernels for the two finite-dimensional Gaussian field terminals.

  1. def OAI.InvariantIsing.vectorTerminalBackward line 13
  2. def OAI.InvariantIsing.vectorTerminalUpdate line 17
  3. def OAI.InvariantIsing.vectorTerminalMultiplier line 20
  4. lemma OAI.InvariantIsing.measurable_vectorTerminalBackward line 25
  5. lemma OAI.InvariantIsing.measurable_vectorTerminalUpdate line 30
  6. lemma OAI.InvariantIsing.measurable_vectorTerminalMultiplier line 33
  7. lemma OAI.InvariantIsing.vectorTerminalMultiplier_moment line 40
  8. def OAI.InvariantIsing.vectorTerminalAncestorKernel line 51
  9. lemma OAI.InvariantIsing.vectorTerminalAncestorKernel_markov line 60
  10. lemma OAI.InvariantIsing.vectorTerminalAncestorKernel_seed line 71