OAI/Probability/FreeIsing/Posterior/ArrayPosteriorStationarity.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Problem367.measurable_arrayNaturalFiltration_of_intertwining line 15
  2. theorem OAI.Problem367.ae_all_nnrealTimePrimitive_eq_of_version line 34
  3. def OAI.Problem367.ArrayPosteriorStationarity.plantedRelabel line 58
  4. def OAI.Problem367.ArrayPosteriorStationarity.spinArray line 63
  5. lemma OAI.Problem367.ArrayPosteriorStationarity.measurable_spinArray line 66
  6. def OAI.Problem367.ArrayPosteriorStationarity.filtration line 70
  7. lemma OAI.Problem367.ArrayPosteriorStationarity.measurable_plantedRelabel_filtration line 76
  8. lemma OAI.Problem367.ArrayPosteriorStationarity.measurable_plantedRelabel_symm_filtration line 87
  9. lemma OAI.Problem367.ArrayPosteriorStationarity.measurePreserving_plantedRelabel line 98
  10. lemma OAI.Problem367.ArrayPosteriorStationarity.integrable_spin_coordinate line 106
  11. def OAI.Problem367.ArrayPosteriorStationarity.posterior line 117
  12. lemma OAI.Problem367.ArrayPosteriorStationarity.measurable_posterior line 124
  13. theorem OAI.Problem367.ArrayPosteriorStationarity.posterior_relabel_ae line 130
  14. theorem OAI.Problem367.ArrayPosteriorStationarity.posterior_version_relabel_ae line 146
  15. theorem OAI.Problem367.ArrayPosteriorStationarity.posterior_version_array_relabel_ae line 161
  16. theorem OAI.Problem367.ArrayPosteriorStationarity.posterior_primitive_relabel_ae line 177
  17. theorem OAI.Problem367.ArrayPosteriorStationarity.innovation_array_relabel_ae line 201