OAI/Combinatorics/TreewidthL1/BagLabels.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.BoundedTreewidthL1.BagLabels.Local line 10
2. def OAI.BoundedTreewidthL1.BagLabels.assemble line 11
3. def OAI.BoundedTreewidthL1.BagLabels.restrict line 14
4. def OAI.BoundedTreewidthL1.BagLabels.globalMass line 16
5. lemma OAI.BoundedTreewidthL1.BagLabels.coherent_equal line 24
6. lemma OAI.BoundedTreewidthL1.BagLabels.assemble_on_support line 42
7. lemma OAI.BoundedTreewidthL1.BagLabels.expectation_global line 62
8. lemma OAI.BoundedTreewidthL1.BagLabels.expectation_local line 77
9. theorem OAI.BoundedTreewidthL1.BagLabels.global_bag_law line 97

   Source documentation

   The canonical junction law is a genuine measure on global vertex labels, with exact connected-subtree marginals. Compatibility is enforced by the local edge support, never assumed for independently sampled bag states.

   theorem global_bag_law (T : SimpleGraph I) (hT : T.IsTree) (B : I → Set V)
       (hcover : ∀ v, ∃ i, v ∈ B i)
       (hrun : ∀ v, (T.induce {i | v ∈ B i}).Preconnected)
       (μ : (i : I) → (B i → Bool) → ℝ)
       (R : (i j : I) → (B i → Bool) → (B j → Bool) → ℝ)
       (hs : TreeMarkov.Symmetric (fun i => B i → Bool) R)
       (hn : TreeMarkov.Normalized (fun i => B i → Bool) T μ R)
       (hcomp : ∀ i j, T.Adj i j → ∀ a b, R i j a b ≠ 0 →
         ∀ v hi hj, a ⟨v,hi⟩ = b ⟨v,hj⟩) :
       let ρ := globalMass T B hcover μ R hs
   …

   Mentions: OAI.BoundedTreewidthL1.TreeMarkov.Symmetric, OAI.BoundedTreewidthL1.TreeMarkov.Normalized, OAI.BoundedTreewidthL1.BagLabels.globalMass

10. def OAI.BoundedTreewidthL1.marginal line 144

    Source documentation

    Pushforward mass at a point, for a finite real nonnegative measure.

    noncomputable def marginal {A C : Type*} [Fintype A]
        (f : A → C) (μ : A → ℝ) (c : C) : ℝ := by
    …

11. def OAI.BoundedTreewidthL1.glueWeights line 151

    Source documentation

    The two-part conditional product, with zero denominator interpreted as zero. Only compatible pairs receive mass.

    noncomputable def glueWeights {A B C : Type*} [Fintype A]
        (f : A → C) (g : B → C) (μ : A → ℝ) (ν : B → ℝ) (a : A) (b : B) : ℝ := by
    …

12. lemma OAI.BoundedTreewidthL1.marginal_nonneg line 160
13. lemma OAI.BoundedTreewidthL1.le_marginal line 166
14. lemma OAI.BoundedTreewidthL1.weight_eq_zero_of_marginal_eq_zero line 176
15. lemma OAI.BoundedTreewidthL1.glueWeights_nonneg line 182
16. lemma OAI.BoundedTreewidthL1.glueWeights_row line 192
17. lemma OAI.BoundedTreewidthL1.glueWeights_swap line 213
18. theorem OAI.BoundedTreewidthL1.glueWeights_marginals line 223
19. def OAI.BoundedTreewidthL1.BagLabels.leftTrace line 240
20. def OAI.BoundedTreewidthL1.BagLabels.rightTrace line 242
21. def OAI.BoundedTreewidthL1.BagLabels.pairMass line 244
22. lemma OAI.BoundedTreewidthL1.BagLabels.glueWeights_map line 248
23. def OAI.BoundedTreewidthL1.BagLabels.overlapSwap line 254
24. lemma OAI.BoundedTreewidthL1.BagLabels.pairMass_symmetric line 261
25. lemma OAI.BoundedTreewidthL1.BagLabels.pairMass_row line 277
26. theorem OAI.BoundedTreewidthL1.BagLabels.bag_couplings line 288
27. def OAI.BoundedTreewidthL1.BagLabels.flip line 319
28. def OAI.BoundedTreewidthL1.BagLabels.flipLocal line 325
29. lemma OAI.BoundedTreewidthL1.BagLabels.marginal_equivariant line 331
30. lemma OAI.BoundedTreewidthL1.BagLabels.pairMass_flip line 341
31. lemma OAI.BoundedTreewidthL1.BagLabels.density_flip line 354
32. theorem OAI.BoundedTreewidthL1.BagLabels.canonical_symmetric line 379
33. def OAI.BoundedTreewidthL1.cutDistance line 402
34. def OAI.BoundedTreewidthL1.finiteCutMap line 407

    Source documentation

    The coordinate function of a vertex in the finite weighted cut space.

    noncomputable def finiteCutMap {V ι : Type*} (w : ι → ℝ)
        (cut : ι → V → Bool) (v : V) : PiLp (1 : ENNReal) (fun _ : ι => ℝ) :=
    …

35. lemma OAI.BoundedTreewidthL1.finiteCutMap_norm_sub line 411
36. theorem OAI.BoundedTreewidthL1.finite_cut_realization line 421
37. lemma OAI.BoundedTreewidthL1.BagLabels.marginal_div line 437
38. lemma OAI.BoundedTreewidthL1.BagLabels.marginal_mul line 446
39. lemma OAI.BoundedTreewidthL1.BagLabels.global_path line 455
40. theorem OAI.BoundedTreewidthL1.BagLabels.canonical_gluing line 493

    Source documentation

    Exact common-positive-mass gluing and genuine finite real L1 realization, from the actual local bag masses. The path assertion concerns full bag states; separator-only projection is a further required transport obligation.

    theorem canonical_gluing (T : SimpleGraph I) (hT : T.IsTree) (B : I → Set V)
        (hcover : ∀ v, ∃ i, v ∈ B i)
        (hrun : ∀ v, (T.induce {i | v ∈ B i}).Preconnected)
        (μ : (i : I) → (B i → Bool) → ℝ) (m : ℝ) (hm : 0 < m)
        (hμ : ∀ i a, 0 ≤ μ i a) (hmass : ∀ i, (∑ a, μ i a) = m)
        (hcons : ∀ i j, T.Adj i j → ∀ c,
          marginal (leftTrace B i j) (μ i) c = marginal (rightTrace B i j) (μ j) c)
        (hflip : ∀ i a, μ i (flip (B i) a) = μ i a) :
        ∃ ρ : (V → Bool) → ℝ,
          (∀ ω, 0 ≤ ρ ω) ∧ (∑ ω, ρ ω) = m ∧
          (∀ ω, ρ (flip V ω) = ρ ω) ∧
          (∀ i a, marginal (fun ω => restrict B ω i) ρ a = μ i a) ∧
    …

    Mentions: OAI.BoundedTreewidthL1.marginal, OAI.BoundedTreewidthL1.BagLabels.leftTrace, OAI.BoundedTreewidthL1.BagLabels.rightTrace, OAI.BoundedTreewidthL1.BagLabels.flip, OAI.BoundedTreewidthL1.BagLabels.restrict