OAI/Probability/InvariantIsing/Fields/PriorMinimumCoordinates.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.priorPerturbationPressureMean_eq_namespaced line 12
  2. lemma OAI.InvariantIsing.penalty_update line 27

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

  3. lemma OAI.InvariantIsing.update_mem_Icc line 41

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

  4. theorem OAI.InvariantIsing.priorPerturbation_minimum_coordinates line 50