OAI/Probability/FreeIsing/Gibbs/PosteriorSymmetry.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem367.spinSign_flip line 13
  2. theorem OAI.Problem367.FinitePosterior.fieldMean_reindex line 18
  3. theorem OAI.Problem367.FinitePosterior.fieldMean_neg_of_equiv line 28
  4. theorem OAI.Problem367.finiteIsingPosteriorMean_neg line 41
  5. theorem OAI.Problem367.finiteIsingPosteriorMean_zero line 57
  6. theorem OAI.Problem367.finiteGibbsSpinMean_zero line 66
  7. theorem OAI.Problem367.finiteGibbsSpinMean_neg line 71
  8. theorem OAI.Problem367.infiniteGibbsSpinMean_zero line 78
  9. theorem OAI.Problem367.infiniteGibbsSpinMean_neg_of_tendsto line 85
  10. theorem OAI.Problem367.brownian_ising_array_zero_ae line 97
  11. theorem OAI.Problem367.infiniteGibbsSpinMean_brownian_zero line 110
  12. theorem OAI.Problem367.HasFreeIsingLaw.brownian_past_posterior_zero line 122