OAI/Probability/InvariantIsing/Fields/PriorTensorMinimum.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Compact perturbation minima for a fixed constrained spin/leaf prior.

  1. def OAI.InvariantIsing.priorPerturbationPressureMean line 12
  2. def OAI.InvariantIsing.priorPerturbationObjective line 21
  3. lemma OAI.InvariantIsing.priorTensorLog_integrable line 28
  4. lemma OAI.InvariantIsing.priorPerturbationPressureMean_modulus line 48
  5. lemma OAI.InvariantIsing.continuous_priorPerturbationObjective line 106
  6. lemma OAI.InvariantIsing.priorFiniteBox_minimum line 134
  7. theorem OAI.InvariantIsing.priorPerturbationObjective_exists_minimum line 153