OAI/Probability/InvariantIsing/Fields/PriorFieldDerivative.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The right field derivative of the actual centered constrained-prior pressure, allowing zero and repeated field-variance levels.

  1. def OAI.InvariantIsing.priorNamespacedMeanPressure line 15
  2. def OAI.InvariantIsing.priorFieldCGFMean line 22
  3. def OAI.InvariantIsing.priorFieldInsertionMean line 33
  4. lemma OAI.InvariantIsing.priorFieldCGFMean_right_derivative line 41
  5. lemma OAI.InvariantIsing.priorFieldInsertionMean_right_derivative line 66
  6. lemma OAI.InvariantIsing.priorFieldInsertedLog_cgf_fold line 89
  7. theorem OAI.InvariantIsing.priorNamespacedMeanPressure_field_insert line 113
  8. theorem OAI.InvariantIsing.priorNamespacedMeanPressure_field_right_derivative line 152