OAI/Probability/InvariantIsing/Arrays/ReplicaProductContinuity.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The replica product is a bounded continuous function of the total overlap when the synchronized group factors are bounded and continuous.

  1. lemma OAI.InvariantIsing.replicaProductFirst_eq_min line 14
  2. lemma OAI.InvariantIsing.replicaProductSecond_eq_max line 21
  3. lemma OAI.InvariantIsing.continuous_replicaProductFirst line 28
  4. lemma OAI.InvariantIsing.continuous_replicaProductSecond line 33
  5. def OAI.InvariantIsing.replicaProductKernel line 39
  6. lemma OAI.InvariantIsing.replicaProductKernel_abs_le line 42
  7. lemma OAI.InvariantIsing.continuous_replicaProductKernel line 58
  8. def OAI.InvariantIsing.replicaProductValue line 76
  9. lemma OAI.InvariantIsing.replicaProductValue_abs_le line 79
  10. lemma OAI.InvariantIsing.continuous_replicaProductValue line 94
  11. lemma OAI.InvariantIsing.replicaProductPath_eq_value line 102