OAI/Probability/InvariantIsing/Fields/SpinPriorMinimumCoordinates.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A joint constrained-prior minimum gives the two actual coordinate minima.

  1. lemma OAI.InvariantIsing.spinPriorPerturbationPressureMean_eq_namespaced line 11
  2. lemma OAI.InvariantIsing.penalty_update line 22

    Also declared: OAI/Probability/InvariantIsing/Arrays/TensorPerturbationObjective.lean:22 (same declaration text), OAI/Probability/InvariantIsing/Fields/PriorMinimumCoordinates.lean:27 (same declaration text).

  3. lemma OAI.InvariantIsing.update_mem_Icc line 36

    Also declared: OAI/Probability/InvariantIsing/Arrays/TensorPerturbationObjective.lean:36 (same declaration text), OAI/Probability/InvariantIsing/Fields/PriorMinimumCoordinates.lean:41 (same declaration text).

  4. theorem OAI.InvariantIsing.spinPriorPerturbation_minimum_coordinates line 45