OAI/Probability/FreeIsing/Posterior/SelectedPosteriorStationarity.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.selectedObservationField line 12
  2. def OAI.Problem367.selectedPosterior line 18
  3. theorem OAI.Problem367.selectedObservationField_le line 25
  4. theorem OAI.Problem367.measurable_selectedPosterior line 38
  5. theorem OAI.Problem367.selectedObservationField_comap_relabel line 46
  6. theorem OAI.Problem367.selectedObservationField_le_of_range_subset line 55
  7. theorem OAI.Problem367.selectedObservationField_eq_of_range_eq line 77
  8. theorem OAI.Problem367.selectedPosterior_relabel_ae line 85
  9. theorem OAI.Problem367.selectedPosterior_identDistrib_relabel line 112
  10. theorem OAI.Problem367.selectedPosterior_secondMoment_relabel line 137
  11. theorem OAI.Problem367.selectedPosterior_identDistrib_of_range_relabel line 151