OAI/Probability/FreeIsing/Trees/NoisyConeSeparation.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.PathSideBranches.noisyRegionArray line 12
  2. theorem OAI.Problem367.PathSideBranches.measurable_noisyRegionArray line 17
  3. def OAI.Problem367.PathSideBranches.decodeCone line 22
  4. theorem OAI.Problem367.PathSideBranches.measurable_decodeCone line 30
  5. theorem OAI.Problem367.PathSideBranches.decodeCone_relabel line 37
  6. def OAI.Problem367.PathSideBranches.decodeConeComplement line 46
  7. theorem OAI.Problem367.PathSideBranches.measurable_decodeConeComplement line 57
  8. theorem OAI.Problem367.PathSideBranches.decodeConeComplement_relabel line 68
  9. theorem OAI.Problem367.HasFreeIsingLaw.condIndepFun_noisy_cone_complement line 90
  10. theorem OAI.Problem367.HasFreeIsingLaw.condIndepFun_noisy_sideCone_complement line 117