OAI/Probability/SKBarriers/Interpolation/RestrictedReplicas.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SK.Analytic.ReplicaConfig line 14
  2. def OAI.SK.Analytic.replicaEnergy line 16
  3. def OAI.SK.Analytic.restrictedPartition line 19
  4. def OAI.SK.Analytic.restrictedLogPartition line 22
  5. def OAI.SK.Analytic.replicaRow line 25
  6. def OAI.SK.Analytic.replicaMarginal line 28
  7. theorem OAI.SK.Analytic.restrictedPartition_pos line 31
  8. theorem OAI.SK.Analytic.replicaRow_nonneg line 35
  9. theorem OAI.SK.Analytic.replicaRow_sum line 39
  10. theorem OAI.SK.Analytic.replicaMarginal_nonneg line 44
  11. theorem OAI.SK.Analytic.replicaMarginal_sum line 54
  12. theorem OAI.SK.Analytic.replicaMarginal_energy line 69
  13. theorem OAI.SK.Analytic.continuous_replicaEnergy line 89
  14. theorem OAI.SK.Analytic.continuous_restrictedPartition line 93
  15. theorem OAI.SK.Analytic.continuous_restrictedLogPartition line 97
  16. theorem OAI.SK.Analytic.continuous_replicaRow line 101
  17. theorem OAI.SK.Analytic.continuous_replicaMarginal line 106
  18. theorem OAI.SK.Analytic.restrictedLogPartition_hasDerivAt line 118
  19. def OAI.SK.Analytic.restrictedModel line 136