OAI/Combinatorics/TreewidthL1/ExpandedTree.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BoundedTreewidthL1.ExpandedTree.marginalLaw line 12
2. def OAI.BoundedTreewidthL1.ExpandedTree.jointLaw line 13
3. lemma OAI.BoundedTreewidthL1.ExpandedTree.jointLaw_symm line 14
4. def OAI.BoundedTreewidthL1.ExpandedTree.law line 22
5. lemma OAI.BoundedTreewidthL1.ExpandedTree.normalized line 28
6. theorem OAI.BoundedTreewidthL1.ExpandedTree.law_marginals line 48

   Source documentation

   The expanded-state law is an actual finite tree law of the original common mass. All local state marginals are as prescribed; no gluing existence is assumed.

   theorem law_marginals (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 → ∀ a b, 0 ≤ J i j a b)
       (hrow : ∀ i j, T.Adj i j → ∀ a, ∑ b, J i j a b = μ i a) :
       (∀ x, 0 ≤ law T M μ J hs x) ∧ (∑ x, law T M μ J hs x) = M ∧
         ∀ i a, (∑ x : I → A, if x i = a then law T M μ J hs x else 0) = μ i a := by
   …

   Mentions: OAI.BoundedTreewidthL1.TreeMarkov.Symmetric, OAI.BoundedTreewidthL1.ExpandedTree.law

7. lemma OAI.BoundedTreewidthL1.ExpandedTree.path_expectation line 74
8. lemma OAI.BoundedTreewidthL1.ExpandedTree.support_joint line 89
9. def OAI.BoundedTreewidthL1.ExpandedTree.assemble line 100

   Source documentation

   Gluing of GLOBAL state labels along the running-intersection bags.

   noncomputable def assemble {V : Type*} (B : I → Set V) (hcover : ∀ v, ∃ i, v ∈ B i)
       (label : A → V → Bool) (x : I → A) : V → Bool :=
   …

10. lemma OAI.BoundedTreewidthL1.ExpandedTree.assembled_label line 104
11. lemma OAI.BoundedTreewidthL1.ExpandedTree.law_labels line 120
12. theorem OAI.BoundedTreewidthL1.ExpandedTree.law_path_product line 140

    Source documentation

    On every actual bag-tree path, the law is the genuine product of the prescribed expanded couplings, even though their common mass is not one.

    theorem law_path_product (M : ℝ) (hM : 0 < M) (μ : ℕ → A → ℝ)
        (Q : ℕ → A → A → ℝ)
        (hQ : ∀ n a b, 0 ≤ Q n a b)
        (_ : ∀ n a, (∑ b, Q n a b) = μ n a)
        (hcol : ∀ n b, (∑ a, Q n a b) = μ (n+1) b)
        (n : ℕ) (J : Fin (n+1) → Fin (n+1) → A → A → ℝ)
        (hs : TreeMarkov.Symmetric (fun _ : Fin (n+1) => A) J)
        (hJ : ∀ (i : Fin n) a b, J i.castSucc i.succ a b = Q i.val a b) (x : Fin (n+1) → A) :
        law (SimpleGraph.pathGraph (n+1)) M (fun i => μ i.val) J hs x =
          MarkovProduct.weight (fun _ => A) (μ 0) (MarkovProduct.couplingKernel (fun _ => A) μ Q) n x := by
    …

    Mentions: OAI.BoundedTreewidthL1.TreeMarkov.Symmetric, OAI.BoundedTreewidthL1.ExpandedTree.law, OAI.BoundedTreewidthL1.MarkovProduct.weight, OAI.BoundedTreewidthL1.MarkovProduct.couplingKernel

13. theorem OAI.BoundedTreewidthL1.averaged_cut_realization line 184