OAI/Combinatorics/TreewidthL1/ExpandedAnchor.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BoundedTreewidthL1.ParticleBatch.pairIndex line 20
2. def OAI.BoundedTreewidthL1.ParticleBatch.PairUnique line 22
3. lemma OAI.BoundedTreewidthL1.ParticleBatch.pairIndex_mem line 25
4. lemma OAI.BoundedTreewidthL1.ParticleBatch.PairUnique.mono line 31
5. lemma OAI.BoundedTreewidthL1.ParticleBatch.PairUnique.empty line 36
6. lemma OAI.BoundedTreewidthL1.ParticleBatch.PairUnique.update line 42
7. lemma OAI.BoundedTreewidthL1.ParticleBatch.launchBatch_unique line 71
8. theorem OAI.BoundedTreewidthL1.AnchorTreeParticles.state_unique line 109

   Source documentation

   All simultaneously reserved pairs are disjoint in the ACTUAL depth-recursive branching preparation. In particular every strictly older active reservation avoids both indices reserved by the fresh own-bag launch.

   theorem state_unique (R : RootedForest I) (bag : I → Finset V) (A : I → Finset J)
       (g : I → J → V → ℝ) (k q : ℕ) (hN : Fintype.card ι = 2*q+k.factorial+2)
       (hbag : ∀ i, (bag i).card ≤ k) (hA : ∀ i, (A i).card ≤ q) :
       ∀ i, PairUnique (A i) (state (ι := ι) R bag A g i).2 := by
   …

   Mentions: OAI.BoundedTreewidthL1.RootedForest, OAI.BoundedTreewidthL1.AnchorTreeParticles.state

9. lemma OAI.BoundedTreewidthL1.ExpandedAnchor.parent_antisymm line 136
10. def OAI.BoundedTreewidthL1.ExpandedAnchor.law line 145
11. lemma OAI.BoundedTreewidthL1.ExpandedAnchor.retained_functions line 154
12. lemma OAI.BoundedTreewidthL1.ExpandedAnchor.measurable_law line 173
13. theorem OAI.BoundedTreewidthL1.ExpandedAnchor.realization line 197

    Source documentation

    Actual expanded-state law and its average L1 metric. No consistency or measurable gluing choice is part of the hypotheses.

    theorem realization
        (G : SimpleGraph V) (hG : G.Connected) (ℓ : G.edgeSet → ℝ) (hℓ : ∀ e, 0 < ℓ e)
        (T : SimpleGraph I) (hT : T.IsTree) (root : I) (B : I → Finset V)
        (hcover : ∀ v, ∃ i, v ∈ B i)
        (hedge : ∀ u v, G.Adj u v → ∃ i, u ∈ B i ∧ v ∈ B i)
        (hrun : ∀ v, (T.induce {i | v ∈ B i}).Preconnected)
        (A : I → Finset I) (k q : ℕ) (hbag : ∀ i, (B i).card ≤ k)
        (hA : ∀ i, (A i).card ≤ q) (hN : Fintype.card ι = 2*q+k.factorial+2)
        (ν : Measure Ω) [IsProbabilityMeasure ν]
        (L H Δ : ℝ) (hL : 0 < L) (hH : 0 < H) (hΔ : 0 < Δ)
        (g : Ω → I → I → V → ℝ)
        (hg : ∀ i a v, Measurable (fun ω => g ω i a v))
    …