OAI/Analysis/SeparableQuotients/BranchPaths.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SeparableQuotient.BinaryNodes.child line 9
  2. def OAI.SeparableQuotient.BinaryNodes.ancestors line 11
  3. def OAI.SeparableQuotient.BinaryNodes.branch line 16
  4. lemma OAI.SeparableQuotient.BinaryNodes.child_pos line 20
  5. lemma OAI.SeparableQuotient.BinaryNodes.lt_child line 21
  6. lemma OAI.SeparableQuotient.BinaryNodes.child_parent line 22
  7. lemma OAI.SeparableQuotient.BinaryNodes.child_injective line 25
  8. lemma OAI.SeparableQuotient.BinaryNodes.ancestors_child line 28
  9. lemma OAI.SeparableQuotient.BinaryNodes.ancestors_nonempty line 37
  10. lemma OAI.SeparableQuotient.BinaryNodes.ancestors_mem_le line 42
  11. lemma OAI.SeparableQuotient.BinaryNodes.ancestors_branch line 53
  12. lemma OAI.SeparableQuotient.BinaryNodes.ancestors_branch_length line 63
  13. lemma OAI.SeparableQuotient.BinaryNodes.branch_strict line 66
  14. lemma OAI.SeparableQuotient.BinaryNodes.branch_same_level line 69
  15. lemma OAI.SeparableQuotient.BinaryNodes.exists_separating_node line 73
  16. lemma OAI.SeparableQuotient.ActualSpace.RawPath.code_congr_prefix line 87
  17. structure OAI.SeparableQuotient.ActualSpace.TreeNode line 101
  18. def OAI.SeparableQuotient.ActualSpace.TreeNode.initial line 116
  19. def OAI.SeparableQuotient.ActualSpace.TreeNode.lookup line 121
  20. def OAI.SeparableQuotient.ActualSpace.TreeNode.rawAlong line 123
  21. def OAI.SeparableQuotient.ActualSpace.TreeNode.nodeCode line 129
  22. def OAI.SeparableQuotient.ActualSpace.TreeNode.requested line 133
  23. lemma OAI.SeparableQuotient.ActualSpace.TreeNode.requested_pos line 136
  24. def OAI.SeparableQuotient.ActualSpace.TreeNode.listSupport line 143
  25. lemma OAI.SeparableQuotient.ActualSpace.TreeNode.mem_listSupport line 146
  26. def OAI.SeparableQuotient.ActualSpace.TreeNode.nextStart line 150
  27. def OAI.SeparableQuotient.ActualSpace.TreeNode.next line 152
  28. lemma OAI.SeparableQuotient.ActualSpace.TreeNode.next_start line 161
  29. lemma OAI.SeparableQuotient.ActualSpace.TreeNode.next_weight line 162
  30. lemma OAI.SeparableQuotient.ActualSpace.TreeNode.next_metadata_gt line 164
  31. lemma OAI.SeparableQuotient.ActualSpace.TreeNode.next_rho line 170
  32. def OAI.SeparableQuotient.ActualSpace.TreeNode.state line 181
  33. def OAI.SeparableQuotient.ActualSpace.TreeNode.node line 185
  34. lemma OAI.SeparableQuotient.ActualSpace.TreeNode.state_eq_ofFn line 187
  35. lemma OAI.SeparableQuotient.ActualSpace.TreeNode.state_length line 196
  36. lemma OAI.SeparableQuotient.ActualSpace.TreeNode.lookup_state line 198
  37. lemma OAI.SeparableQuotient.ActualSpace.TreeNode.mem_state line 201
  38. lemma OAI.SeparableQuotient.ActualSpace.TreeNode.finish_le_start line 205
  39. lemma OAI.SeparableQuotient.ActualSpace.TreeNode.metadata_strict line 210
  40. lemma OAI.SeparableQuotient.ActualSpace.TreeNode.support_before line 214
  41. lemma OAI.SeparableQuotient.ActualSpace.TreeNode.successive_vector line 221
  42. lemma OAI.SeparableQuotient.ActualSpace.TreeNode.successive_piece line 227
  43. lemma OAI.SeparableQuotient.ActualSpace.TreeNode.nodeCode_eq_branch line 233
  44. lemma OAI.SeparableQuotient.ActualSpace.TreeNode.nodeCode_lookup line 249
  45. lemma OAI.SeparableQuotient.ActualSpace.TreeNode.weight_rule line 265
  46. def OAI.SeparableQuotient.ActualSpace.TreeNode.branchPath line 278

    Source documentation

    The prescribed-weight exact-pair construction yields actual admissible paths on all infinite binary branches; records include all original metadata.

    def branchPath (b : ℕ → Bool) : InfinitePath f where
…
  47. lemma OAI.SeparableQuotient.ActualSpace.TreeNode.cross_evaluate line 309
  48. lemma OAI.SeparableQuotient.ActualSpace.TreeNode.pathPartial_node line 322
  49. lemma OAI.SeparableQuotient.ActualSpace.TreeNode.pathPartial_other line 334
  50. lemma OAI.SeparableQuotient.ActualSpace.TreeNode.pathFunctional_node line 341
  51. lemma OAI.SeparableQuotient.ActualSpace.TreeNode.pathFunctional_other line 351
  52. lemma OAI.SeparableQuotient.ActualSpace.TreeNode.pair_mem_submodule line 356
  53. lemma OAI.SeparableQuotient.ActualSpace.TreeNode.restricted_separated line 365

    Source documentation

    Path restrictions are uniformly separated on every subspace containing the block sequence, with separation constant 1/500.

    lemma restricted_separated (V : Submodule ℝ E) (hV : ∀ n, z.embed n ∈ V)
    {b c : ℕ → Bool} (hbc : b ≠ c) :
    (1/1000 : ℝ) ≤ ‖(pathFunctional (branchPath z b)).comp V.subtypeL -
      (pathFunctional (branchPath z c)).comp V.subtypeL‖ := by
…

    Mentions: OAI.SeparableQuotient.ActualSpace.E, OAI.SeparableQuotient.ActualSpace.pathFunctional, OAI.SeparableQuotient.ActualSpace.TreeNode.branchPath