OAI/Combinatorics/MatrixRemoval/SampledPath.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

Concrete common-leaf path positions. The variable-position type is Fin (2*h+1) × Fin (2^h): even classes are plus, odd classes are minus, and class 2*h is the shared leaf class.

  1. abbrev OAI.Problem348.SampledPath.VariablePosition line 13
  2. def OAI.Problem348.SampledPath.blockSize line 15
  3. theorem OAI.Problem348.SampledPath.blockSize_pos line 17
  4. theorem OAI.Problem348.SampledPath.blockSize_mul_nodes line 20
  5. def OAI.Problem348.SampledPath.mix line 25

    Source documentation

    Retain the sampled leaf's node but choose the within-node offset from u.

    def mix (b z u : ℕ) : ℕ := z / b * b + u % b
  6. theorem OAI.Problem348.SampledPath.mix_lt line 27
  7. theorem OAI.Problem348.SampledPath.mix_div line 34
  8. theorem OAI.Problem348.SampledPath.mix_mod line 40
  9. def OAI.Problem348.SampledPath.mixFin line 46
  10. theorem OAI.Problem348.SampledPath.mixFin_node line 55
  11. theorem OAI.Problem348.SampledPath.mixFin_root line 59
  12. theorem OAI.Problem348.SampledPath.mixFin_leaf line 64
  13. def OAI.Problem348.SampledPath.classAt line 70

    Source documentation

    The plus and minus names coincide precisely at the leaf level.

    def classAt (h i : ℕ) (hi : i ≤ h) (plus : Bool) : Fin (2 * h + 1) :=
…
  14. theorem OAI.Problem348.SampledPath.classAt_depth line 76
  15. theorem OAI.Problem348.SampledPath.classAt_leaf line 85
  16. theorem OAI.Problem348.SampledPath.classAt_internal line 89
  17. theorem OAI.Problem348.SampledPath.classAt_leaf_iff line 93
  18. theorem OAI.Problem348.SampledPath.classAt_signs_eq_iff line 103
  19. def OAI.Problem348.SampledPath.sample line 110
  20. def OAI.Problem348.SampledPath.depth line 114
  21. def OAI.Problem348.SampledPath.node line 116
  22. theorem OAI.Problem348.SampledPath.sample_depth line 119
  23. theorem OAI.Problem348.SampledPath.sample_node line 123
  24. theorem OAI.Problem348.SampledPath.sample_node_lt line 130
  25. theorem OAI.Problem348.SampledPath.sample_nodes_eq line 138

    Source documentation

    The two axes may use different offset seeds and still follow one common path.

    theorem sample_nodes_eq (h i : ℕ) (hi : i ≤ h) (s t : Bool)
    (z u v : Fin (2 ^ h)) :
    node (sample h i hi s z u) = node (sample h i hi t z v) := by
…

    Mentions: OAI.Problem348.SampledPath.node, OAI.Problem348.SampledPath.sample

  26. theorem OAI.Problem348.SampledPath.ancestor_parent line 143
  27. theorem OAI.Problem348.SampledPath.sample_parent line 149
  28. theorem OAI.Problem348.SampledPath.sample_shared_leaf line 156
  29. theorem OAI.Problem348.SampledPath.sample_leaf_offset line 161
  30. theorem OAI.Problem348.SampledPath.sample_root_offset line 165
  31. theorem OAI.Problem348.SampledPath.sample_root_node line 169