OAI/Probability/FreeIsing/Trees/ConeCoding.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.TreeConeCoding.encode line 12
  2. theorem OAI.Problem367.TreeConeCoding.encode_nil line 16
  3. theorem OAI.Problem367.TreeConeCoding.length_encode line 18
  4. theorem OAI.Problem367.TreeConeCoding.chain_encode line 24
  5. theorem OAI.Problem367.TreeConeCoding.encode_injective line 31
  6. theorem OAI.Problem367.TreeConeCoding.encode_surjective line 48
  7. def OAI.Problem367.TreeConeCoding.continuationEquiv line 62
  8. theorem OAI.Problem367.TreeConeCoding.encode_take line 70
  9. theorem OAI.Problem367.TreeConeCoding.chain_append_iff line 79
  10. def OAI.Problem367.TreeConeCoding.vertex line 85
  11. theorem OAI.Problem367.TreeConeCoding.vertex_val line 90
  12. theorem OAI.Problem367.TreeConeCoding.vertex_nil line 94
  13. theorem OAI.Problem367.TreeConeCoding.length_vertex line 99
  14. theorem OAI.Problem367.TreeConeCoding.vertex_prefix line 103
  15. theorem OAI.Problem367.TreeConeCoding.vertex_injective line 106
  16. theorem OAI.Problem367.TreeConeCoding.vertex_surjective_cone line 112
  17. def OAI.Problem367.TreeConeCoding.coneEquiv line 125
  18. theorem OAI.Problem367.TreeConeCoding.vertex_take line 133
  19. def OAI.Problem367.TreeConeCoding.labels line 142
  20. theorem OAI.Problem367.TreeConeCoding.measurable_labels line 146
  21. theorem OAI.Problem367.TreeConeCoding.map_labels line 151
  22. theorem OAI.Problem367.TreeConeCoding.measurePreserving_labels line 158
  23. theorem OAI.Problem367.TreeConeCoding.map_uniform_labels line 166