OAI/Combinatorics/TreewidthL1/MarkovProduct.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.BoundedTreewidthL1.MarkovProduct.History line 10
2. def OAI.BoundedTreewidthL1.MarkovProduct.weight line 11
3. def OAI.BoundedTreewidthL1.MarkovProduct.forward line 14
4. lemma OAI.BoundedTreewidthL1.MarkovProduct.weight_snoc line 25
5. lemma OAI.BoundedTreewidthL1.MarkovProduct.sum_history_snoc line 39
6. lemma OAI.BoundedTreewidthL1.MarkovProduct.terminal_marginal line 46
7. lemma OAI.BoundedTreewidthL1.MarkovProduct.forward_total line 72
8. theorem OAI.BoundedTreewidthL1.MarkovProduct.product_law line 84

   Source documentation

   Normalization and the exact terminal marginal of the product measure.

   theorem product_law (p : L 0 → ℝ) (K : (i : ℕ) → L i → L (i+1) → ℝ)
       (hp : ∀ a, 0 ≤ p a) (hp₁ : (∑ a, p a) = 1)
       (hK : ∀ i a b, 0 ≤ K i a b) (hK₁ : ∀ i a, (∑ b, K i a b) = 1) (n : ℕ) :
       (∀ x, 0 ≤ weight L p K n x) ∧ (∑ x, weight L p K n x) = 1 ∧
         ∀ b : L n, (∑ x : History L n, if x (Fin.last n) = b then weight L p K n x else 0) =
           forward L p K n b := by
   …

   Mentions: OAI.BoundedTreewidthL1.MarkovProduct.weight, OAI.BoundedTreewidthL1.MarkovProduct.History, OAI.BoundedTreewidthL1.MarkovProduct.forward

9. theorem OAI.BoundedTreewidthL1.MarkovProduct.last_pair line 100

   Source documentation

   The product has its prescribed final adjacent-pair marginal, including zero-probability states and transitions.

   theorem last_pair (p : L 0 → ℝ) (K : (i : ℕ) → L i → L (i+1) → ℝ)
       (n : ℕ) (a : L n) (b : L (n+1)) :
       (∑ x : History L (n+1),
         if x (Fin.last n).castSucc = a ∧ x (Fin.last (n+1)) = b
         then weight L p K (n+1) x else 0) = forward L p K n a * K n a b := by
   …

   Mentions: OAI.BoundedTreewidthL1.MarkovProduct.History, OAI.BoundedTreewidthL1.MarkovProduct.weight, OAI.BoundedTreewidthL1.MarkovProduct.forward

10. def OAI.BoundedTreewidthL1.MarkovProduct.couplingKernel line 124

    Source documentation

    Transition obtained from a prescribed adjacent-pair marginal. A zero-mass row is filled with the next marginal; the row is never visited.

    noncomputable def couplingKernel (μ : (i : ℕ) → L i → ℝ)
        (J : (i : ℕ) → L i → L (i+1) → ℝ)
        (i : ℕ) (a : L i) (b : L (i+1)) : ℝ :=
    …

11. def OAI.BoundedTreewidthL1.MarkovProduct.historyPrefix line 129
12. lemma OAI.BoundedTreewidthL1.MarkovProduct.joint_zero_row line 138
13. lemma OAI.BoundedTreewidthL1.MarkovProduct.couplingKernel_stochastic line 148
14. lemma OAI.BoundedTreewidthL1.MarkovProduct.couplingKernel_balance line 166
15. lemma OAI.BoundedTreewidthL1.MarkovProduct.coupling_forward line 176
16. lemma OAI.BoundedTreewidthL1.MarkovProduct.prefix_snoc line 190
17. lemma OAI.BoundedTreewidthL1.MarkovProduct.prefix_expectation line 202

    Source documentation

    Integrating out a stochastic suffix preserves the complete historyPrefix law, not only one-coordinate marginals.

    lemma prefix_expectation (p : L 0 → ℝ) (K : (i : ℕ) → L i → L (i+1) → ℝ)
        (hK₁ : ∀ i a, (∑ b, K i a b) = 1)
        (m n : ℕ) (hmn : m ≤ n) (f : History L m → ℝ) :
        (∑ x : History L n, weight L p K n x * f (historyPrefix L m n hmn x)) =
          ∑ x : History L m, weight L p K m x * f x := by
    …

    Mentions: OAI.BoundedTreewidthL1.MarkovProduct.History, OAI.BoundedTreewidthL1.MarkovProduct.weight, OAI.BoundedTreewidthL1.MarkovProduct.historyPrefix

18. theorem OAI.BoundedTreewidthL1.MarkovProduct.coupling_chain line 227