OAI/Probability/DilutedSpin/ColoredAnchor.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DilutedSpinGlass.PrescribedTree.protectedAt line 13

   Source documentation

   All leaves protected, at a general positive insertion, not just along a single direction. This retains the original finite-kernel law.

   noncomputable def protectedAt {n : ℕ} (S : PrescribedTree n)
       (T : KernelTower Ω n) (m : Fin (n+1) → ℝ) (G : Sample Ω S → ℝ)
       (A : FinitePath Ω n → ℝ) : ℝ :=
   …

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

2. lemma OAI.DilutedSpinGlass.PrescribedTree.hasDerivAt_protectedAt line 20
3. lemma OAI.DilutedSpinGlass.PrescribedTree.hasDerivAt_protectedAt_varying line 77
4. def OAI.DilutedSpinGlass.PrescribedTree.anchorAt line 108

   Source documentation

   A subset of old positions remains unused. Every used old position and all fresh colored positions are canceled.

   noncomputable def anchorAt {n : ℕ} (S : PrescribedTree n)
       (T : KernelTower Ω n) (m : Fin (n+1) → ℝ) {ι : Type} (U : Finset ι)
       (paths : ι → Sample Ω S → FinitePath Ω n) (G : Sample Ω S → ℝ)
       (A : FinitePath Ω n → ℝ) : ℝ :=
   …

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

5. lemma OAI.DilutedSpinGlass.PrescribedTree.protectedAt_sum line 114
6. lemma OAI.DilutedSpinGlass.PrescribedTree.hasDerivAt_anchorAt line 121
7. def OAI.DilutedSpinGlass.pathCoordinate line 166
8. def OAI.DilutedSpinGlass.PrescribedTree.leafEdge line 172
9. lemma OAI.DilutedSpinGlass.PrescribedTree.edgeDepth_leafEdge line 177
10. lemma OAI.DilutedSpinGlass.PrescribedTree.coordinate_pathAt line 185
11. lemma OAI.DilutedSpinGlass.PrescribedTree.leafEdge_eq_iff line 196

    Source documentation

    Sharing the actual depth-(i+1) vertex is exactly the split-depth inequality. Equality of sampled spin/mark values plays no role in this fact.

    lemma leafEdge_eq_iff {n : ℕ} (S : PrescribedTree n) (a b : S.Leaf) (i : Fin n) :
        leafEdge S a i = leafEdge S b i ↔ i.val+1 ≤ splitDepth S a b := by
    …

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.leafEdge, OAI.DilutedSpinGlass.PrescribedTree.splitDepth