OAI/Combinatorics/TreewidthL1/Construction.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BoundedTreewidthL1.ExpandedConstruction.weight_total line 13
2. lemma OAI.BoundedTreewidthL1.ExpandedConstruction.edge_label line 24
3. def OAI.BoundedTreewidthL1.ExpandedConstruction.joints line 42
4. lemma OAI.BoundedTreewidthL1.ExpandedConstruction.joints_symmetric line 49
5. lemma OAI.BoundedTreewidthL1.ExpandedConstruction.joints_eq line 62
6. lemma OAI.BoundedTreewidthL1.ExpandedConstruction.joints_coupling line 73
7. lemma OAI.BoundedTreewidthL1.ExpandedConstruction.joints_label line 94
8. lemma OAI.BoundedTreewidthL1.ExpandedConstruction.weight_separation line 120
9. def OAI.BoundedTreewidthL1.ExpandedConstruction.ensemble line 141
10. lemma OAI.BoundedTreewidthL1.ExpandedConstruction.ensemble_data line 149
11. lemma OAI.BoundedTreewidthL1.ExpandedConstruction.ensemble_labels line 174
12. lemma OAI.BoundedTreewidthL1.ExpandedConstruction.ensemble_cobag line 190

    Source documentation

    Every bag has the exact particle metric, while the inter-bag coupling is chosen to retain the sweep order of each currently reserved particle.

    lemma ensemble_cobag (T : SimpleGraph I) (hT : T.IsTree) (parent : I → Option I)
        (horient : ∀ i j, T.Adj i j → parent i = some j ∨ parent j = some i)
        (hanti : ∀ i j, parent i = some j → parent j ≠ some i)
        (M : ℝ) (hM : 0 < M) (hι : 0 < Fintype.card ι)
        (F : I → ι → V → ℝ) (B : I → Finset V)
        (hcover : ∀ v, ∃ i, v ∈ B i) (hrun : ∀ v, (T.induce {i | v ∈ B i}).Preconnected)
        (fresh₁ fresh₂ : I → ι) (C : I → Finset ι)
        (hret : ∀ i j, parent j = some i → ∀ r ∈ C j, F i r = F j r)
        (htrace : ∀ i j, parent j = some i → particleTrace M (F i) (B j) = particleTrace M (F j) (B j))
        (i : I) (hF : ∀ r v, |F i r v| ≤ M) (u v : V) (hu : u ∈ B i) (hv : v ∈ B i) :
        cutDistance (ensemble T parent hanti M F B fresh₁ fresh₂ C)
          (ExpandedTree.assemble (fun i => (B i : Set V)) hcover label) u v =
    …

    Mentions: OAI.BoundedTreewidthL1.particleTrace, OAI.BoundedTreewidthL1.cutDistance, OAI.BoundedTreewidthL1.ExpandedConstruction.ensemble, OAI.BoundedTreewidthL1.ExpandedTree.assemble

13. lemma OAI.BoundedTreewidthL1.ExpandedMeasurable.selected line 246
14. lemma OAI.BoundedTreewidthL1.ExpandedMeasurable.measurable_marginal line 256
15. lemma OAI.BoundedTreewidthL1.ExpandedMeasurable.measurable_glue line 266
16. lemma OAI.BoundedTreewidthL1.ExpandedMeasurable.measurable_edge_fixed line 275
17. lemma OAI.BoundedTreewidthL1.ExpandedMeasurable.measurable_edge line 286
18. lemma OAI.BoundedTreewidthL1.ExpandedMeasurable.measurable_joints line 297
19. lemma OAI.BoundedTreewidthL1.ExpandedMeasurable.measurable_law line 313
20. lemma OAI.BoundedTreewidthL1.ExpandedMeasurable.measurable_ensemble line 333

    Source documentation

    Measurability of the actual expanded tree law, allowing the reservation indices and free pools to depend on all the previously sampled noise.

    lemma measurable_ensemble [MeasurableSpace ι] [MeasurableSingletonClass ι]
        (T : SimpleGraph I) (parent : I → Option I)
        (hanti : ∀ i j, parent i = some j → parent j ≠ some i)
        (M : ℝ) (F : Ω → I → ι → V → ℝ) (B : I → Finset V)
        (hF : ∀ i a, Measurable (fun ω => weight M (F ω i) a))
        (fresh₁ fresh₂ : Ω → I → ι) (C : Ω → I → Finset ι)
        (h₁ : ∀ i, Measurable (fun ω => fresh₁ ω i)) (h₂ : ∀ i, Measurable (fun ω => fresh₂ ω i))
        (hC : ∀ i, Measurable (fun ω => C ω i)) (x : I → State ι V) :
        Measurable (fun ω => ensemble T parent hanti M (F ω) B (fresh₁ ω) (fresh₂ ω) (C ω) x) := by
    …