OAI/Probability/FKMaps/NodeOrder.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.FKCRT.TreeCoding.recordTypeAt_congr_prefix line 11
  2. lemma OAI.FKCRT.TreeCoding.record_boundary line 18
  3. def OAI.FKCRT.Inventory.labelProfileSum line 61
  4. lemma OAI.FKCRT.Inventory.labelProfileSum_empty line 65
  5. lemma OAI.FKCRT.Inventory.labelProfileSum_attach line 68
  6. lemma OAI.FKCRT.Inventory.toCode_labelProfile line 145
  7. def OAI.FKCRT.Inventory.CoreTree.before line 189
  8. def OAI.FKCRT.Inventory.CoreTree.after line 192
  9. lemma OAI.FKCRT.Inventory.CoreTree.children_split line 195
  10. lemma OAI.FKCRT.Inventory.CoreTree.before_length line 201
  11. lemma OAI.FKCRT.Inventory.CoreTree.after_length line 204
  12. lemma OAI.FKCRT.Inventory.CoreTree.labels_split line 207
  13. lemma OAI.FKCRT.Inventory.CoreTree.labels_nonempty line 211
  14. def OAI.FKCRT.Inventory.CoreTree.nodeIndex line 214
  15. lemma OAI.FKCRT.Inventory.CoreTree.nodeIndex_bound line 219
  16. lemma OAI.FKCRT.Inventory.CoreTree.labels_take_child line 232
  17. lemma OAI.FKCRT.Inventory.CoreTree.forest_labels_degrees line 243
  18. lemma OAI.FKCRT.Inventory.CoreTree.forest_labels_properties line 250
  19. lemma OAI.FKCRT.Inventory.CoreTree.labels_take_nonneg line 256
  20. def OAI.FKCRT.Inventory.CoreTree.nodeSpine line 264
  21. lemma OAI.FKCRT.Inventory.CoreTree.nodeSpine_profile line 269
  22. lemma OAI.FKCRT.Inventory.CoreTree.nodeSpine_marked line 285
  23. lemma OAI.FKCRT.Inventory.CoreTree.coreIncrement_slot line 289
  24. lemma OAI.FKCRT.Inventory.CoreTree.nodeSpine_metric line 298
  25. theorem OAI.FKCRT.Inventory.CoreTree.routeLength_marked line 311

    Source documentation

    The actual original-map pole distance is the same marked ancestor sum appearing in the conditioned-code uniform LLN, not a separately sampled tree.

    theorem routeLength_marked (t : CoreTree) (v : t.Node) :
    (t.routeLength v:ℝ)=markedSpineSum coreIncrement t.toCode (t.nodeIndex_bound v).le
      (fun i => t.labels[i.val]) := by
…

    Mentions: OAI.FKCRT.Inventory.CoreTree, OAI.FKCRT.Inventory.coreIncrement

  26. def OAI.FKCRT.Inventory.CoreTree.depth line 316
  27. lemma OAI.FKCRT.Inventory.CoreTree.nodeSpine_one line 321
  28. lemma OAI.FKCRT.Inventory.CoreTree.depth_height line 331
  29. lemma OAI.FKCRT.Inventory.CoreTree.offset_separation line 347
  30. lemma OAI.FKCRT.Inventory.CoreTree.children_index_strict line 357
  31. lemma OAI.FKCRT.Inventory.CoreTree.children_order line 365
  32. lemma OAI.FKCRT.Inventory.CoreTree.nodeIndex_root line 372
  33. lemma OAI.FKCRT.Inventory.CoreTree.routeLength_root line 373
  34. lemma OAI.FKCRT.Inventory.CoreTree.same_child_between line 375
  35. lemma OAI.FKCRT.Inventory.CoreTree.commonRoute_le_intervening line 392

    Source documentation

    Every intervening preorder vertex remains below the last common ancestor.

    lemma commonRoute_le_intervening (t : CoreTree) (v w u : t.Node)
    (h₁ : t.nodeIndex v≤t.nodeIndex u) (h₂ : t.nodeIndex u≤t.nodeIndex w) :
    t.commonRoute v w≤t.routeLength u := by
…

    Mentions: OAI.FKCRT.Inventory.CoreTree

  36. lemma OAI.FKCRT.Inventory.CoreTree.exists_intervening_low line 415

    Source documentation

    One intervening vertex is either the ancestor itself or the first node of its selected right-hand child, costing at most one maximum core degree.

    lemma exists_intervening_low (t : CoreTree) (v w : t.Node) (h : t.nodeIndex v≤t.nodeIndex w) :
    ∃ u : t.Node,t.nodeIndex v≤t.nodeIndex u ∧ t.nodeIndex u≤t.nodeIndex w ∧
      t.routeLength u≤t.commonRoute v w+t.maxDegree := by
…

    Mentions: OAI.FKCRT.Inventory.CoreTree

  37. lemma OAI.FKCRT.Inventory.CoreTree.flatMap_find_index line 447
  38. lemma OAI.FKCRT.Inventory.CoreTree.nodeIndex_surjective line 461

    Source documentation

    The literal recursive node index covers every and only preorder cell.

    lemma nodeIndex_surjective (t : CoreTree) {r : ℕ} (hr : r<t.labels.length) :
    ∃ v : t.Node,t.nodeIndex v=r := by
…

    Mentions: OAI.FKCRT.Inventory.CoreTree

  39. theorem OAI.FKCRT.Inventory.CoreTree.pole_walk_comparison line 482

    Source documentation

    A walk minimum can be used without assuming a probabilistic law at a random ancestor. This is the deterministic all-poles comparison after the uniform same-code ancestral estimate.

    theorem pole_walk_comparison (t : CoreTree) (v w m : t.Node) (a b : t.Dart)
    (ha : t.pole v=some a) (hb : t.pole w=some b)
    (hm₁ : t.nodeIndex v≤t.nodeIndex m) (hm₂ : t.nodeIndex m≤t.nodeIndex w)
    (W : t.Node → ℝ) {α ε : ℝ} (hα : 0≤α)
    (herr : ∀ u,|(t.routeLength u:ℝ)-α*W u|≤ε)
    (hmin : ∀ u,t.nodeIndex v≤t.nodeIndex u → t.nodeIndex u≤t.nodeIndex w → W m≤W u) :
    |t.realDistance a b-α*(W v+W w-2*W m)|≤4*(t.maxDegree:ℝ)+4*ε := by
…

    Mentions: OAI.FKCRT.Inventory.CoreTree