OAI/Combinatorics/TreewidthL1/TreeGeometry.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BoundedTreewidthL1.RootedTree.downPath_take line 10
2. lemma OAI.BoundedTreewidthL1.RootedTree.depth_getVert line 15
3. lemma OAI.BoundedTreewidthL1.RootedTree.downPath_getVert_getVert line 19
4. lemma OAI.BoundedTreewidthL1.RootedTree.parent_getVert line 23
5. lemma OAI.BoundedTreewidthL1.TreeCache.inclusive_getVert line 41
6. lemma OAI.BoundedTreewidthL1.TreeCache.active_getVert line 54
7. def OAI.BoundedTreewidthL1.RootedTree.pathIndex line 68
8. lemma OAI.BoundedTreewidthL1.RootedTree.pathIndex_comap line 78
9. def OAI.BoundedTreewidthL1.ExpandedTree.pathJoint line 108
10. lemma OAI.BoundedTreewidthL1.ExpandedTree.pathJoint_coupling line 112
11. lemma OAI.BoundedTreewidthL1.ExpandedTree.endpoint_path_product line 133

    Source documentation

    Restriction of an actual tree law to its unique endpoint path, in the un-normalized coupling-product convention used by the reservation tests.

    lemma endpoint_path_product (T : SimpleGraph I) (hT : T.IsTree) (M : ℝ) (hM : 0 < M)
        (μ : I → A → ℝ) (J : I → I → A → A → ℝ) (hs : TreeMarkov.Symmetric (fun _ : I => A) J)
        (hμ : ∀ i a, 0 ≤ μ i a) (hmass : ∀ i, (∑ a, μ i a) = M)
        (hJ : ∀ i j, T.Adj i j → IsCoupling (μ i) (μ j) (J i j))
        (Y Z : I) (f : A → A → ℝ) :
        (∑ x : I → A, law T M μ J hs x * f (x Y) (x Z)) =
          ∑ x : Fin ((RootedTree.forest T hT Y).depth Z + 1) → A,
            MarkovProduct.weight (fun _ => A) (μ Y)
              (MarkovProduct.couplingKernel (fun _ => A)
                (fun s => μ ((RootedTree.downPath T hT Y Z).getVert s))
                (pathJoint T μ J (RootedTree.downPath T hT Y Z)))
              ((RootedTree.forest T hT Y).depth Z) x *
    …

    Mentions: OAI.BoundedTreewidthL1.TreeMarkov.Symmetric, OAI.BoundedTreewidthL1.ExpandedTree.law, OAI.BoundedTreewidthL1.RootedTree.forest, OAI.BoundedTreewidthL1.MarkovProduct.weight, OAI.BoundedTreewidthL1.MarkovProduct.couplingKernel, OAI.BoundedTreewidthL1.RootedTree.downPath, OAI.BoundedTreewidthL1.ExpandedTree.pathJoint

12. lemma OAI.BoundedTreewidthL1.ExpandedConstruction.ensemble_endpoint line 183
13. lemma OAI.BoundedTreewidthL1.RootedTree.append_path line 224
14. lemma OAI.BoundedTreewidthL1.RootedTree.exists_join_index line 238

    Source documentation

    The common root prefixes terminate at one finite, deterministic index.

    lemma exists_join_index : ∃ s : ℕ,
        s ≤ (forest T hT root).depth X ∧ s ≤ (forest T hT root).depth Y ∧
        (downPath T hT root X).getVert s = (downPath T hT root Y).getVert s ∧
        ∀ a b, a ≤ (forest T hT root).depth X → b ≤ (forest T hT root).depth Y →
          (downPath T hT root X).getVert a = (downPath T hT root Y).getVert b → a = b ∧ a ≤ s := by
    …

    Mentions: OAI.BoundedTreewidthL1.RootedTree.forest, OAI.BoundedTreewidthL1.RootedTree.downPath

15. lemma OAI.BoundedTreewidthL1.RootedTree.path_at_join line 263

    Source documentation

    At the meet, the two descending arms form exactly the unique Y--X path.

    lemma path_at_join (s : ℕ)
        (hsx : s ≤ (forest T hT root).depth X) (hsy : s ≤ (forest T hT root).depth Y)
        (hs : (downPath T hT root X).getVert s = (downPath T hT root Y).getVert s)
        (hmax : ∀ a b, a ≤ (forest T hT root).depth X → b ≤ (forest T hT root).depth Y →
          (downPath T hT root X).getVert a = (downPath T hT root Y).getVert b → a = b ∧ a ≤ s) :
        downPath T hT Y X =
          (((downPath T hT root Y).drop s).reverse.copy rfl hs.symm).append
            ((downPath T hT root X).drop s) := by
    …

    Mentions: OAI.BoundedTreewidthL1.RootedTree.forest, OAI.BoundedTreewidthL1.RootedTree.downPath

16. lemma OAI.BoundedTreewidthL1.RootedTree.join_suffix line 290
17. lemma OAI.BoundedTreewidthL1.RootedTree.join_length line 303
18. structure OAI.BoundedTreewidthL1.ExpandedConstruction.TreeData line 320

    Source documentation

    Data of the actual constructed ensemble. Retention and trace identities are verified by the particle recursion, not axioms about its endpoint map.

    structure TreeData (T : SimpleGraph I) (M : ℝ) where
    …

19. def OAI.BoundedTreewidthL1.ExpandedConstruction.TreeData.dist line 335
20. def OAI.BoundedTreewidthL1.ExpandedConstruction.TreeData.chain line 338
21. lemma OAI.BoundedTreewidthL1.ExpandedConstruction.TreeData.chain_coupling line 341
22. lemma OAI.BoundedTreewidthL1.ExpandedConstruction.TreeData.chain_eq line 346
23. lemma OAI.BoundedTreewidthL1.ExpandedConstruction.TreeData.height_test line 359
24. lemma OAI.BoundedTreewidthL1.ExpandedConstruction.TreeData.launch_test line 394
25. lemma OAI.BoundedTreewidthL1.TreeCache.active_on_path line 445
26. lemma OAI.BoundedTreewidthL1.TreeCache.active_self line 452
27. lemma OAI.BoundedTreewidthL1.TreeCache.path_ne line 458
28. lemma OAI.BoundedTreewidthL1.TreeCache.pair_transport line 467

    Source documentation

    The actual inclusive tree cache transports an anchor's entire function and its indices throughout every interval up to its last active bag.

    lemma pair_transport (S : I → (ι → V → ℝ) × (I → ι × ι))
        (hpairs : ∀ i p, (forest T hT root).parent i = some p →
          ∀ a ∈ active T hT root B D k d J i ∩ active T hT root B D k d J p,
          (S i).2 a = (S p).2 a ∧
          (S i).1 ((S i).2 a).1 = (S p).1 ((S p).2 a).1 ∧
          (S i).1 ((S i).2 a).2 = (S p).1 ((S p).2 a).2)
        (e a t : ℕ) (he : e ≤ (forest T hT root).depth X)
        (ha : a ∈ inclusiveCache k (bags T hT root B X) d (heights T hT root D X) J e)
        (hat : a ≤ t) (hte : t ≤ e) :
        let v := (downPath T hT root X).getVert
    …

    Mentions: OAI.BoundedTreewidthL1.TreeCache.active, OAI.BoundedTreewidthL1.TreeCache.bags, OAI.BoundedTreewidthL1.TreeCache.heights

29. lemma OAI.BoundedTreewidthL1.AnchorTreeParticles.state_congr_depth line 497
30. lemma OAI.BoundedTreewidthL1.AnchorTreeParticles.predecessor_congr_depth line 516
31. lemma OAI.BoundedTreewidthL1.AnchorTreeParticles.singleton_launch line 529
32. lemma OAI.BoundedTreewidthL1.AnchorTreeParticles.singleton_positive line 541

    Source documentation

    The frozen positive particle is an affine function of its OWN fresh noise; its baseline is computed entirely before that node is processed.

    lemma singleton_positive (R : RootedForest I) (B : I → Finset V) (A : I → Finset J)
        (g : I → J → V → ℝ) (i : I) (a : J) (hfresh : fresh R A i = {a})
        (hdistinct : ((state (ι := ι) R B A g i).2 a).1 ≠ ((state R B A g i).2 a).2) :
    …

    Mentions: OAI.BoundedTreewidthL1.RootedForest, OAI.BoundedTreewidthL1.AnchorTreeParticles.fresh, OAI.BoundedTreewidthL1.AnchorTreeParticles.state