OAI/Probability/FreeIsing/Trees/InwardCutFields.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.PathSideBranches.regionGaussianField line 12
  2. def OAI.Problem367.PathSideBranches.inwardGaussianField line 20
  3. def OAI.Problem367.PathSideBranches.cutInwardGaussianField line 24
  4. theorem OAI.Problem367.PathSideBranches.measurable_regionGaussianField_noisyRegion line 29
  5. theorem OAI.Problem367.PathSideBranches.measurable_cutInwardGaussianField_noisyRegion line 37
  6. theorem OAI.Problem367.PathSideBranches.cone_takeVertex_antitone line 45
  7. theorem OAI.Problem367.PathSideBranches.parent_takeVertex_succ line 50
  8. theorem OAI.Problem367.PathSideBranches.takeVertex_not_mem_next_cone line 57
  9. theorem OAI.Problem367.PathSideBranches.takeVertex_succ_ne_nil line 65
  10. theorem OAI.Problem367.PathSideBranches.diff_union_compl_of_subset line 73
  11. theorem OAI.Problem367.PathSideBranches.diff_union_diff_of_subset line 86
  12. theorem OAI.Problem367.PathSideBranches.inward_cut_difference_step line 99
  13. theorem OAI.Problem367.PathSideBranches.inward_cut_difference_initial line 135