OAI/Probability/FreeIsing/Trees/RootedGeometry.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem367.image_child_depth_le line 7
  2. theorem OAI.Problem367.image_depth_le_of_root_fixed line 17
  3. theorem OAI.Problem367.treeAut_length_eq_of_root_fixed line 32
  4. theorem OAI.Problem367.treeAut_preimage_depthBall line 43
  5. theorem OAI.Problem367.treeAut_image_depthBall line 50
  6. theorem OAI.Problem367.treeAut_preimage_depthSphere line 61