OAI/Probability/FreeIsing/Posterior/ProgressiveIsingPosterior.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.finiteGibbsSpinMean line 17
  2. theorem OAI.Problem367.continuous_finiteGibbsSpinMean line 24
  3. def OAI.Problem367.infiniteGibbsSpinMean line 29
  4. theorem OAI.Problem367.measurable_infiniteGibbsSpinMean line 33
  5. theorem OAI.Problem367.infiniteGibbsSpinMean_abs_le_one line 41
  6. theorem OAI.Problem367.HasFreeIsingLaw.infiniteGibbsSpinMean_eq_posterior line 46
  7. theorem OAI.Problem367.isStronglyProgressive_infiniteGibbsSpinMean line 74
  8. theorem OAI.Problem367.HasFreeIsingLaw.infiniteGibbsSpinMean_eq_brownian_past line 86
  9. theorem OAI.Problem367.measurable_spinSign_array line 146
  10. theorem OAI.Problem367.HasFreeIsingLaw.exists_bounded_progressive_brownian_posterior line 151
  11. theorem OAI.Problem367.HasFreeIsingLaw.infiniteGibbsSpinMean_brownian_field_bound line 183