OAI/Combinatorics/TreewidthL1/TreeMarkov.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.BoundedTreewidthL1.TreeMarkov.Symmetric line 14

   Source documentation

   A symmetric edge interaction; nonedge values are irrelevant.

   abbrev Symmetric (R : (i j : I) → A i → A j → ℝ) : Prop :=
   …

2. def OAI.BoundedTreewidthL1.TreeMarkov.edgeFactor line 17
3. def OAI.BoundedTreewidthL1.TreeMarkov.density line 21
4. def OAI.BoundedTreewidthL1.TreeMarkov.Normalized line 28

   Source documentation

   The exact local normalization needed for junction gluing. At zero-mass states no conditional probability is required.

   def Normalized (T : SimpleGraph I) (μ : (i : I) → A i → ℝ)
       (R : (i j : I) → A i → A j → ℝ) : Prop :=
   …

5. lemma OAI.BoundedTreewidthL1.TreeMarkov.edgeFactor_mk line 41
6. lemma OAI.BoundedTreewidthL1.TreeMarkov.density_nonneg line 47
7. lemma OAI.BoundedTreewidthL1.TreeMarkov.density_zero line 57
8. lemma OAI.BoundedTreewidthL1.TreeMarkov.edgeFinset_leaf line 66
9. lemma OAI.BoundedTreewidthL1.TreeMarkov.edgeFactor_induce line 99
10. lemma OAI.BoundedTreewidthL1.TreeMarkov.density_leaf line 110
11. lemma OAI.BoundedTreewidthL1.TreeMarkov.splitAt_here line 139
12. lemma OAI.BoundedTreewidthL1.TreeMarkov.splitAt_away line 145
13. lemma OAI.BoundedTreewidthL1.TreeMarkov.splitAt_restrict line 152
14. lemma OAI.BoundedTreewidthL1.TreeMarkov.sum_leaf_density line 157
15. lemma OAI.BoundedTreewidthL1.TreeMarkov.expectation_leaf line 176
16. lemma OAI.BoundedTreewidthL1.TreeMarkov.Normalized.induce line 194
17. theorem OAI.BoundedTreewidthL1.TreeMarkov.node_marginal_card line 201
18. theorem OAI.BoundedTreewidthL1.TreeMarkov.tree_density line 254

    Source documentation

    Canonical root-independent tree density and exact one-node marginals. Zero-mass states, deterministic edges and arbitrary finite state spaces allowed.

    theorem tree_density (T : SimpleGraph I) (hT : T.IsTree)
        (μ : (i : I) → A i → ℝ) (R : (i j : I) → A i → A j → ℝ)
        (hs : Symmetric A R) (hn : Normalized A T μ R) :
        (∀ x, 0 ≤ density A T μ R hs x) ∧
        (∑ x, density A T μ R hs x) = 1 ∧
        ∀ i a, (∑ x, if x i = a then density A T μ R hs x else 0) = μ i a := by
    …

    Mentions: OAI.BoundedTreewidthL1.TreeMarkov.Symmetric, OAI.BoundedTreewidthL1.TreeMarkov.Normalized, OAI.BoundedTreewidthL1.TreeMarkov.density

19. lemma OAI.BoundedTreewidthL1.TreeMarkov.tree_path_mem_connected line 276
20. lemma OAI.BoundedTreewidthL1.TreeMarkov.exists_leaf_outside line 291

    Source documentation

    A proper connected subtree can be pruned from outside without altering it.

    lemma exists_leaf_outside {I : Type*} [Fintype I] (T : SimpleGraph I) (hT : T.IsTree)
        (S : Set I) (hc : (T.induce S).Connected) (hproper : S ≠ Set.univ) :
        ∃ l : I, l ∉ S ∧ T.degree l = 1 := by
    …

21. lemma OAI.BoundedTreewidthL1.TreeMarkov.edgeFinset_comap_equiv line 331
22. lemma OAI.BoundedTreewidthL1.TreeMarkov.density_equiv line 355
23. lemma OAI.BoundedTreewidthL1.TreeMarkov.expectation_surjective line 372
24. theorem OAI.BoundedTreewidthL1.TreeMarkov.expectation_comap_card line 406
25. theorem OAI.BoundedTreewidthL1.TreeMarkov.expectation_comap line 453

    Source documentation

    Exact connected-subtree marginal of the canonical junction law. In particular this applies to a simple bag path, before projection to intersection assignments.

    theorem expectation_comap (T : SimpleGraph I) (hT : T.IsTree)
        (μ : (i : I) → A i → ℝ) (R : (i j : I) → A i → A j → ℝ)
        (hs : Symmetric A R) (hn : Normalized A T μ R)
        {J : Type*} [Fintype J] (e : J ↪ I) (hc : (T.comap e).Connected)
        (f : ((j : J) → A (e j)) → ℝ) :
        (∑ x, density A T μ R hs x * f (fun j => x (e j))) =
          ∑ x, density (fun j => A (e j)) (T.comap e) (fun j => μ (e j))
            (fun j k => R (e j) (e k)) (fun j k => hs (e j) (e k)) x * f x := by
    …

    Mentions: OAI.BoundedTreewidthL1.TreeMarkov.Symmetric, OAI.BoundedTreewidthL1.TreeMarkov.Normalized, OAI.BoundedTreewidthL1.TreeMarkov.density

26. def OAI.BoundedTreewidthL1.TreeMarkov.interaction line 470

    Source documentation

    Interaction constructed from the actual local pair mass, not assumed.

    noncomputable def interaction (μ : (i : I) → A i → ℝ)
        (J : (i j : I) → A i → A j → ℝ) (i j : I) (a : A i) (b : A j) : ℝ :=
    …

27. lemma OAI.BoundedTreewidthL1.TreeMarkov.interaction_symmetric line 474
28. lemma OAI.BoundedTreewidthL1.TreeMarkov.interaction_normalized line 482
29. theorem OAI.BoundedTreewidthL1.TreeMarkov.coupling_tree line 515

    Source documentation

    Canonical tree law from genuinely consistent adjacent pair distributions. No positive lower bound on local state probabilities is imposed.

    theorem coupling_tree (T : SimpleGraph I) (hT : T.IsTree)
        (μ : (i : I) → A i → ℝ) (J : (i j : I) → A i → A j → ℝ)
        (hμ : ∀ i a, 0 ≤ μ i a) (hμ₁ : ∀ i, (∑ a, μ i a) = 1)
        (hs : Symmetric A J)
        (hJ : ∀ i j, T.Adj i j → ∀ a b, 0 ≤ J i j a b)
        (hrow : ∀ i j, T.Adj i j → ∀ a, (∑ b, J i j a b) = μ i a) :
        let R := interaction A μ J
    …

    Mentions: OAI.BoundedTreewidthL1.TreeMarkov.Symmetric, OAI.BoundedTreewidthL1.TreeMarkov.interaction

30. abbrev OAI.BoundedTreewidthL1.MarkovFlow.History line 542
31. def OAI.BoundedTreewidthL1.MarkovFlow.IsMarkovLaw line 544

    Source documentation

    Same finite stochastic-product definition as the exact CKR obligation.

    def IsMarkovLaw {r : ℕ} (L : Fin (r + 1) → Type*) [∀ i, Fintype (L i)]
        (μ : History L → ℝ) : Prop :=
    …

    Mentions: OAI.BoundedTreewidthL1.MarkovFlow.History

32. def OAI.BoundedTreewidthL1.TreeMarkov.pathEdge line 556
33. lemma OAI.BoundedTreewidthL1.TreeMarkov.path_edges line 568
34. lemma OAI.BoundedTreewidthL1.TreeMarkov.path_density line 598
35. lemma OAI.BoundedTreewidthL1.TreeMarkov.product_factorization line 608
36. theorem OAI.BoundedTreewidthL1.TreeMarkov.path_markov line 642

    Source documentation

    The canonical marginal on any simple bag-tree path is an actual Markov product, not merely a collection of consistent adjacent marginals.

    theorem path_markov (μ : (i : Fin (r+1)) → A i → ℝ)
        (R : (i j : Fin (r+1)) → A i → A j → ℝ) (hs : Symmetric A R)
        (hn : Normalized A (SimpleGraph.pathGraph (r+1)) μ R) :
        MarkovFlow.IsMarkovLaw A (density A (SimpleGraph.pathGraph (r+1)) μ R hs) := by
    …

    Mentions: OAI.BoundedTreewidthL1.TreeMarkov.Symmetric, OAI.BoundedTreewidthL1.TreeMarkov.Normalized, OAI.BoundedTreewidthL1.MarkovFlow.IsMarkovLaw, OAI.BoundedTreewidthL1.TreeMarkov.density