OAI/Probability/DilutedSpin/MarkerConcrete.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DilutedSpinGlass.PrescribedTree.markerFresh_split line 13
2. def OAI.DilutedSpinGlass.PrescribedTree.markerColorEquiv line 21
3. def OAI.DilutedSpinGlass.PrescribedTree.markerColorTarget line 24
4. def OAI.DilutedSpinGlass.PrescribedTree.markerColorFresh line 28
5. def OAI.DilutedSpinGlass.PrescribedTree.markerColorOld line 32
6. lemma OAI.DilutedSpinGlass.PrescribedTree.markerColorTarget_bijective line 36
7. lemma OAI.DilutedSpinGlass.PrescribedTree.markerColorJoint_bijective line 40
8. lemma OAI.DilutedSpinGlass.PrescribedTree.markerColorTarget_split line 48
9. lemma OAI.DilutedSpinGlass.PrescribedTree.marker_spatialProduct line 58
10. theorem OAI.DilutedSpinGlass.PrescribedTree.concrete_marker_covariance line 74

    Source documentation

    Concrete marker geometry at every preceding depth. In particular all bijections and separation requirements of the history identity are produced, not standing assumptions. The color count is positive for every tree.

    theorem concrete_marker_covariance (μ : Measure Z) (Ω : Z → Type) [∀ z, Fintype (Ω z)]
        (A : PrescribedTree n) (r : ℕ) (a : (stem (unary A) r).Leaf)
        (K : (z : Z) → KernelTower (Ω z) (n+1+r)) (m : Fin (n+1+r+1) → ℝ)
        (hm : StrictMono m) (hp : ∀ j, 0 ≤ m j) (hend : m (Fin.last (n+1+r))=1)
        (V : (z : Z) → FinitePath (Ω z) (n+1+r) → Fin N → ℝ) :
        matrixRootCovariance μ Ω (stem (markerFork A) r) (stem (unary A) r)
          (markerColorTarget A r) K m
          (List.ofFn (fun c : Fin (Fintype.card A.Leaf) => (some c : Option (Fin (Fintype.card A.Leaf))))).reverse a
          (fun z => spatialProduct (fun c x i => match c with | none => 1 | some _ => V z x i))
          (fun z => treeOverlap (stem (unary A) r) (V z)) =
        partialKappa (stem (markerFork A) r) m (Finset.univ.image (markerColorTarget A r)) *
          ((∫ z, ((stem (doubled A) r).sampleLaw (K z)).expect (fun w =>
    …

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.stem, OAI.DilutedSpinGlass.PrescribedTree.unary, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.matrixRootCovariance, OAI.DilutedSpinGlass.PrescribedTree.markerFork, OAI.DilutedSpinGlass.PrescribedTree.markerColorTarget, OAI.DilutedSpinGlass.PrescribedTree.spatialProduct, OAI.DilutedSpinGlass.PrescribedTree.treeOverlap, OAI.DilutedSpinGlass.PrescribedTree.partialKappa, OAI.DilutedSpinGlass.PrescribedTree.doubled, OAI.DilutedSpinGlass.PrescribedTree.sampleLaw