OAI/Combinatorics/TreewidthL1/ExpandedParticles.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.BoundedTreewidthL1.anchor_embedding_preparation line 11
2. lemma OAI.BoundedTreewidthL1.marginal_mono line 137
3. lemma OAI.BoundedTreewidthL1.marginal_add line 145
4. lemma OAI.BoundedTreewidthL1.marginal_smul line 155
5. lemma OAI.BoundedTreewidthL1.marginal_comp line 165
6. lemma OAI.BoundedTreewidthL1.marginal_total line 184
7. lemma OAI.BoundedTreewidthL1.glueWeights_row_formula line 191
8. lemma OAI.BoundedTreewidthL1.glueWeights_col_formula line 204
9. theorem OAI.BoundedTreewidthL1.glueWeights_of_submarginal line 217
10. def OAI.BoundedTreewidthL1.ExpandedParticleKernel.compose line 249

    Source documentation

    A finite transition coupling. We compose couplings, not stochastic kernels, so zero-mass states require no arbitrary probability distribution.

    noncomputable def compose {A B C : Type*} [Fintype B]
        (μ : B → ℝ) (J : A → B → ℝ) (K : B → C → ℝ) (a : A) (c : C) : ℝ :=
    …

11. theorem OAI.BoundedTreewidthL1.ExpandedParticleKernel.retained_or_free_marginal line 253
12. theorem OAI.BoundedTreewidthL1.ExpandedParticleKernel.compose_coupling line 291
13. theorem OAI.BoundedTreewidthL1.ExpandedParticleKernel.compose_trace line 337
14. abbrev OAI.BoundedTreewidthL1.ExpandedParticleLaw.State line 359
15. def OAI.BoundedTreewidthL1.ExpandedParticleLaw.label line 361
16. def OAI.BoundedTreewidthL1.ExpandedParticleLaw.weight line 364
17. def OAI.BoundedTreewidthL1.ExpandedParticleLaw.trace line 367
18. def OAI.BoundedTreewidthL1.ExpandedParticleLaw.incomingKey line 371

    Source documentation

    At incoming updates, the entire state is retained on protected particles. Every remaining state is pooled in one free class.

    noncomputable def incomingKey (C : Finset ι) (a : State ι V) : Option (State ι V) :=
    …

    Mentions: OAI.BoundedTreewidthL1.ExpandedParticleLaw.State

19. def OAI.BoundedTreewidthL1.ExpandedParticleLaw.departureKey line 376

    Source documentation

    Departure reheats the fresh pair jointly and every other index separately. Orientation is retained in either case.

    noncomputable def departureKey (a b : ι) (x : State ι V) : ι × Bool :=
    …

    Mentions: OAI.BoundedTreewidthL1.ExpandedParticleLaw.State

20. def OAI.BoundedTreewidthL1.ExpandedParticleLaw.incoming line 379
21. def OAI.BoundedTreewidthL1.ExpandedParticleLaw.departure line 383
22. lemma OAI.BoundedTreewidthL1.ExpandedParticleLaw.weight_nonneg line 387
23. lemma OAI.BoundedTreewidthL1.ExpandedParticleLaw.finite_event line 392
24. lemma OAI.BoundedTreewidthL1.ExpandedParticleLaw.oriented_marginal line 400
25. theorem OAI.BoundedTreewidthL1.ExpandedParticleLaw.trace_marginal line 432

    Source documentation

    Exact original symmetric bag trace; no change of the prepared marginal.

     theorem trace_marginal (M : ℝ) (F : ι → V → ℝ) (P : Finset V) (b : P → Bool) :
        marginal (trace P) (weight M F) b = (particleTrace M F P).real {b} := by
    …

    Mentions: OAI.BoundedTreewidthL1.marginal, OAI.BoundedTreewidthL1.ExpandedParticleLaw.trace, OAI.BoundedTreewidthL1.ExpandedParticleLaw.weight, OAI.BoundedTreewidthL1.particleTrace

26. theorem OAI.BoundedTreewidthL1.ExpandedParticleLaw.incoming_coupling line 456
27. theorem OAI.BoundedTreewidthL1.ExpandedParticleLaw.departure_coupling line 490