OAI/Probability/InvariantIsing/Fields/SpinPriorFieldInsertionLaw.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Independent Gaussian insertion for the actual constrained cascade.

  1. def OAI.InvariantIsing.spinPriorFieldInsertedLog line 13
  2. lemma OAI.InvariantIsing.measurable_spinPriorFieldInsertedLog line 22
  3. lemma OAI.InvariantIsing.spinPriorFieldInsertedLog_conditional_law line 40
  4. lemma OAI.InvariantIsing.tensorField_joint_map_eq line 92

    Also declared: OAI/Probability/InvariantIsing/Arrays/TensorFieldDerivativeLaw.lean:142 (same declaration text).

  5. theorem OAI.InvariantIsing.spinPriorFieldInsertedLog_identDistrib line 110