OAI/Probability/DilutedSpin/TreeMarkLaw.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DilutedSpinGlass.PrescribedTree.Edge line 12

   Source documentation

   Every nonroot vertex is retained, including unary vertices.

   def Edge : {n : ℕ} → PrescribedTree n → Type
     | 0, .leaf => Empty
     | _+1, .node _ C => (i : _) × Option (Edge (C i))

   Mentions: OAI.DilutedSpinGlass.PrescribedTree

2. instance OAI.DilutedSpinGlass.PrescribedTree.edgeFintype line 16
3. def OAI.DilutedSpinGlass.PrescribedTree.edgeDepth line 22
4. def OAI.DilutedSpinGlass.PrescribedTree.vertexValues line 33
5. def OAI.DilutedSpinGlass.PrescribedTree.ofVertexValues line 42
6. lemma OAI.DilutedSpinGlass.PrescribedTree.vertexValues_of line 46
7. lemma OAI.DilutedSpinGlass.PrescribedTree.of_vertexValues line 56
8. def OAI.DilutedSpinGlass.PrescribedTree.vertexEquiv line 65
9. lemma OAI.DilutedSpinGlass.PrescribedTree.sampleLaw_markPrior_weight line 77

   Source documentation

   Under the genuine independent mark prior, vertex marks have the product law at their actual depths. This is a law statement, not a coupling assumption.

   lemma sampleLaw_markPrior_weight {n : ℕ} (S : PrescribedTree n)
       (Q : Fin n → FiniteLaw Ω) (x : Sample Ω S) :
       (S.sampleLaw (markPrior n Q)).weight x =
         ∏ e : Edge S, (Q (edgeDepth S e)).weight (vertexValues S x e) := by
   …

   Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.markPrior, OAI.DilutedSpinGlass.PrescribedTree.Edge, OAI.DilutedSpinGlass.PrescribedTree.edgeDepth, OAI.DilutedSpinGlass.PrescribedTree.vertexValues

10. lemma OAI.DilutedSpinGlass.PrescribedTree.expect_markPrior line 97
11. theorem OAI.DilutedSpinGlass.PrescribedTree.freshEval_const line 120
12. theorem OAI.DilutedSpinGlass.PrescribedTree.grow_projectivity line 132

    Source documentation

    Deleting a newly sampled branch preserves the joint law of ALL old paths. The old test may be arbitrarily correlated with any retained old prefixes.

    theorem grow_projectivity {n : ℕ} (S : PrescribedTree n) (K : KernelTower Ω n)
        (v : Internal S) (H : Sample Ω S → ℝ) :
        (sampleLaw (grow S v) K).expect (fun x => H (oldSample S v x)) =
          (sampleLaw S K).expect H := by
    …

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.PrescribedTree.Internal, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.PrescribedTree.sampleLaw, OAI.DilutedSpinGlass.PrescribedTree.grow, OAI.DilutedSpinGlass.PrescribedTree.oldSample