OAI/Probability/InvariantIsing/Arrays/TensorFieldDerivativeLaw.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Increasing the linear field in a nonnegative monotone direction is exactly an independent Gaussian insertion in the actual tensor model.

  1. lemma OAI.InvariantIsing.tensorNamespacedPath_field_add_cross line 16
  2. def OAI.InvariantIsing.tensorFieldInsertedLog line 37
  3. def OAI.InvariantIsing.tensorFieldInsertedHamiltonian line 46
  4. lemma OAI.InvariantIsing.measurable_tensorFieldInsertedHamiltonian line 53
  5. lemma OAI.InvariantIsing.measurable_tensorFieldInsertedLog line 74
  6. lemma OAI.InvariantIsing.tensorFieldInsertedLog_conditional_law line 91
  7. lemma OAI.InvariantIsing.tensorField_joint_map_eq line 142

    Also declared: OAI/Probability/InvariantIsing/Fields/SpinPriorFieldInsertionLaw.lean:92 (same declaration text).

  8. theorem OAI.InvariantIsing.tensorFieldInsertedLog_identDistrib line 160