OAI/Probability/DilutedSpin/ShapeEmbedding.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DilutedSpinGlass.PrescribedTree.leaf_marginal line 13

   Source documentation

   Every old leaf of a prescribed tree has exactly the full kernel path law.

   theorem leaf_marginal {n : ℕ} (S : PrescribedTree n) (T : KernelTower Ω n)
       (a : S.Leaf) (D : FinitePath Ω n → ℝ) :
       (S.sampleLaw T).expect (fun x => D (S.pathAt a x)) = (KernelTower.law n T).expect D := by
   …

   Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.KernelTower.law

2. lemma OAI.DilutedSpinGlass.PrescribedTree.pathAt_single line 33
3. lemma OAI.DilutedSpinGlass.PrescribedTree.anchorAt_leaf line 45
4. theorem OAI.DilutedSpinGlass.PrescribedTree.anchorCoefficient_leaf line 66

   Source documentation

   The one-test Taylor coefficient is independent of all unused old leaves. This justifies the singleton-anchor term in the prescribed-tree identity.

   theorem anchorCoefficient_leaf {n : ℕ} (S : PrescribedTree n) (T : KernelTower Ω n)
       (m : Fin (n+1) → ℝ) (hm : ∀ j : Fin n, m j.succ ≠ 0)
       (hroot : m 0 = 0) (hend : m (Fin.last n) = 1)
       (a : S.Leaf) (D E : FinitePath Ω n → ℝ) (k : ℕ) :
       anchorCoefficient S T m D a (fun x => E (S.pathAt a x)) k =
         anchorCoefficient (single n) T m D (firstLeaf (single n))
           (fun x => E ((single n).pathAt (firstLeaf (single n)) x)) k := by
   …

   Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.anchorCoefficient, OAI.DilutedSpinGlass.PrescribedTree.single, OAI.DilutedSpinGlass.PrescribedTree.firstLeaf, OAI.DilutedSpinGlass.PrescribedTree.pathAt

5. structure OAI.DilutedSpinGlass.PrescribedTree.SplitMap line 95

   Source documentation

   Inclusion of an exact prescribed splitting matrix into the actual history geometry. This is an inclusion of leaf POSITIONS, not of sampled configurations.

   structure SplitMap {n : ℕ} (T S : PrescribedTree n) where
   …

   Mentions: OAI.DilutedSpinGlass.PrescribedTree

6. lemma OAI.DilutedSpinGlass.PrescribedTree.SplitMap.injective line 102
7. def OAI.DilutedSpinGlass.PrescribedTree.SplitMap.childIndex line 109
8. lemma OAI.DilutedSpinGlass.PrescribedTree.SplitMap.rootAgreement line 112
9. lemma OAI.DilutedSpinGlass.PrescribedTree.SplitMap.childIndex_injective line 120
10. def OAI.DilutedSpinGlass.PrescribedTree.SplitMap.childLeaf line 130
11. lemma OAI.DilutedSpinGlass.PrescribedTree.SplitMap.leaf_eq_child line 133
12. def OAI.DilutedSpinGlass.PrescribedTree.SplitMap.child line 143
13. lemma OAI.DilutedSpinGlass.PrescribedTree.SplitMap.arity_le line 151
14. theorem OAI.DilutedSpinGlass.PrescribedTree.SplitMap.branchingCount_le line 157

    Source documentation

    Exact split constraints force every target branching vertex to occur in the actual history, even when several different vertices have equal depths.

    theorem branchingCount_le {n : ℕ} {T S : PrescribedTree n} (f : SplitMap T S)
        (P : ℕ → Prop) : branchingCount T P ≤ branchingCount S P := by
    …

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.SplitMap, OAI.DilutedSpinGlass.PrescribedTree.branchingCount