OAI/Probability/FKMaps/NodeMetric.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FKCRT.Inventory.CoreTree.Node line 13

    Source documentation

    Actual ordered-tree nodes, with a distinct trivial leaf at every empty corner word. Coincident map poles are not identified as tree nodes.

    def Node : CoreTree → Type
  | .leaf => PUnit
  | .branch c ts => PUnit ⊕ (Σ i : Fin c.val.length,Node (ts i))

    Mentions: OAI.FKCRT.Inventory.CoreTree

  2. instance OAI.FKCRT.Inventory.CoreTree.(instance at line 17) line 17
  3. instance OAI.FKCRT.Inventory.CoreTree.(instance at line 24) line 24
  4. def OAI.FKCRT.Inventory.CoreTree.root line 26
  5. def OAI.FKCRT.Inventory.CoreTree.rootDart line 30
  6. def OAI.FKCRT.Inventory.CoreTree.pole line 34
  7. lemma OAI.FKCRT.Inventory.CoreTree.pole_some line 40
  8. def OAI.FKCRT.Inventory.CoreTree.routeLength line 44
  9. lemma OAI.FKCRT.Inventory.CoreTree.darts_head line 49
  10. lemma OAI.FKCRT.Inventory.CoreTree.pole_none_of_leaf line 60
  11. lemma OAI.FKCRT.Inventory.CoreTree.route_zero_of_leaf line 64
  12. lemma OAI.FKCRT.Inventory.CoreTree.pole_some_of_ne_leaf line 68
  13. theorem OAI.FKCRT.Inventory.CoreTree.distance_root_pole line 76

    Source documentation

    The route length sums the genuine isolated-core graph distances along the strict ancestor chain. It equals the original full-map graph distance from the root pole, rather than a postulated replacement metric.

    theorem distance_root_pole (t : CoreTree) (v : t.Node) (a b : t.Dart)
    (ha : t.rootDart=some a) (hb : t.pole v=some b) :
    t.matching.distance a b=(t.routeLength v : ℕ∞) := by
…

    Mentions: OAI.FKCRT.Inventory.CoreTree

  14. lemma OAI.FKCRT.Inventory.CoreTree.child_interval line 126
  15. theorem OAI.FKCRT.Inventory.CoreTree.child_internal_distance line 145

    Source documentation

    Isometry of every nonempty inserted child, in its original all-edge metric. No root-distance-only surrogate is used.

    theorem child_internal_distance (c : Core) (ts : Fin c.val.length → CoreTree)
    (i : Fin c.val.length) (a x y : (ts i).Dart) (L : List (ts i).Dart)
    (hhead : (ts i).darts=a::L) :
    (branch c ts).matching.distance (childDart ts i x) (childDart ts i y)=
      (ts i).matching.distance x y := by
…

    Mentions: OAI.FKCRT.Inventory.Core, OAI.FKCRT.Inventory.CoreTree, OAI.FKCRT.Inventory.CoreTree.Dart, OAI.FKCRT.Inventory.CoreTree.darts, OAI.FKCRT.Inventory.CoreTree.childDart

  16. lemma OAI.FKCRT.Inventory.CoreTree.child_gate_distance line 174
  17. def OAI.FKCRT.Inventory.CoreTree.childPole line 222
  18. lemma OAI.FKCRT.Inventory.CoreTree.root_and_head line 226
  19. lemma OAI.FKCRT.Inventory.CoreTree.core_to_childPole line 234
  20. lemma OAI.FKCRT.Inventory.CoreTree.childPole_not_child line 248
  21. theorem OAI.FKCRT.Inventory.CoreTree.between_childPoles line 260

    Source documentation

    The exact three-piece route between distinct child components.

    theorem between_childPoles (c : Core) (ts : Fin c.val.length → CoreTree)
    (i j : Fin c.val.length) (hij : i≠j) (v : (ts i).Node) (w : (ts j).Node) :
    (branch c ts).matching.distance (childPole c ts i v) (childPole c ts j w)=
      ((ts i).routeLength v:ℕ∞)+c.matching.distance (nextSlot c i) (nextSlot c j)+
        ((ts j).routeLength w:ℕ∞) := by
…

    Mentions: OAI.FKCRT.Inventory.Core, OAI.FKCRT.Inventory.CoreTree, OAI.FKCRT.Inventory.CoreTree.Node, OAI.FKCRT.Inventory.CoreTree.childPole, OAI.FKCRT.Inventory.CoreTree.routeLength, OAI.FKCRT.Inventory.CoreTree.nextSlot

  22. lemma OAI.FKCRT.Inventory.CoreTree.within_childPoles line 277
  23. def OAI.FKCRT.Inventory.CoreTree.realDistance line 288

    Source documentation

    Real graph distance, on the same literal original map.

    def realDistance (t : CoreTree) (a b : t.Dart) : ℝ :=
…

    Mentions: OAI.FKCRT.Inventory.CoreTree

  24. lemma OAI.FKCRT.Inventory.CoreTree.distance_eq_nat line 292
  25. lemma OAI.FKCRT.Inventory.CoreTree.realDistance_nonneg line 300
  26. lemma OAI.FKCRT.Inventory.CoreTree.realDistance_comm line 302
  27. lemma OAI.FKCRT.Inventory.CoreTree.realDistance_self line 306
  28. lemma OAI.FKCRT.Inventory.CoreTree.real_root_distance line 309
  29. def OAI.FKCRT.Inventory.Core.realDistance line 329
  30. lemma OAI.FKCRT.Inventory.Core.realDistance_nonneg line 332
  31. lemma OAI.FKCRT.Inventory.Core.corner_distance_le line 334
  32. def OAI.FKCRT.Inventory.CoreTree.commonRoute line 345
  33. def OAI.FKCRT.Inventory.CoreTree.maxDegree line 352
  34. lemma OAI.FKCRT.Inventory.CoreTree.maxDegree_core line 356
  35. lemma OAI.FKCRT.Inventory.CoreTree.maxDegree_child line 359
  36. lemma OAI.FKCRT.Inventory.CoreTree.real_between_childPoles line 363
  37. lemma OAI.FKCRT.Inventory.CoreTree.real_within_childPoles line 373
  38. lemma OAI.FKCRT.Inventory.CoreTree.commonRoute_leaf line 383
  39. theorem OAI.FKCRT.Inventory.CoreTree.pole_comparison line 388

    Source documentation

    Exact source two-pole comparison: the only error lies inside the last common ancestor's actual isolated core. All distances use all original edges.

    theorem pole_comparison (t : CoreTree) (v w : t.Node) (a b : t.Dart)
    (ha : t.pole v=some a) (hb : t.pole w=some b) :
    |t.realDistance a b-((t.routeLength v:ℝ)+t.routeLength w-2*t.commonRoute v w)|≤2*t.maxDegree := by
…

    Mentions: OAI.FKCRT.Inventory.CoreTree