OAI/Probability/FreeIsing/Trees/NoisyPathLocality.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.PathSideBranches.noisyRegionSigma line 12
  2. def OAI.Problem367.PathSideBranches.restrictNoisyRegion line 17
  3. theorem OAI.Problem367.PathSideBranches.measurable_restrictNoisyRegion line 22
  4. theorem OAI.Problem367.PathSideBranches.restrictNoisyRegion_array line 28
  5. theorem OAI.Problem367.PathSideBranches.measurable_noisyRegionArray_of_subset line 33
  6. theorem OAI.Problem367.PathSideBranches.noisyRegionSigma_mono line 39
  7. theorem OAI.Problem367.PathSideBranches.noisyRegionSigma_le line 44
  8. theorem OAI.Problem367.PathSideBranches.measurable_later_noisy_forward_observable line 50
  9. theorem OAI.Problem367.PathSideBranches.measurable_later_noisy_forward_product line 61
  10. theorem OAI.Problem367.PathSideBranches.measurable_path_spin_outside_sideCone line 76
  11. theorem OAI.Problem367.HasFreeIsingLaw.condIndepFun_noisy_cone_observables line 93
  12. theorem OAI.Problem367.HasFreeIsingLaw.condIndepFun_noisy_sideCone_observables line 116