OAI/Probability/FreeIsing/Trees/SelectedPathLocality.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem367.selectedObservationField_region_union line 14
  2. theorem OAI.Problem367.selectedObservationField_le_noisyRegionSigma line 35
  3. theorem OAI.Problem367.measurable_selectedPosterior_noisyRegion line 53
  4. theorem OAI.Problem367.measurable_selectedField_noisyRegion line 63
  5. def OAI.Problem367.PathSideBranches.reducedForward line 77
  6. theorem OAI.Problem367.PathSideBranches.target_mem_reducedForward line 81
  7. theorem OAI.Problem367.PathSideBranches.reducedForward_subset_complement line 85
  8. theorem OAI.Problem367.PathSideBranches.forward_eq_reduced_union_side line 89
  9. theorem OAI.Problem367.PathSideBranches.forwardObservationField_eq_reduced_sup_side line 102
  10. theorem OAI.Problem367.PathSideBranches.measurable_later_selectedPosterior line 112
  11. theorem OAI.Problem367.PathSideBranches.measurable_reduced_selectedField line 124
  12. theorem OAI.Problem367.PathSideBranches.measurable_later_selectedPosterior_product line 135