TreeAnchor.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.DilutedSpinGlass.PrescribedTree.pathAt_expect line 12
Source documentation
Every prescribed old leaf has exactly the one-path marginal, including through shared prefixes and arbitrary (possibly unary) stretches.
```
theorem pathAt_expect {n : ℕ} (S : PrescribedTree n) (a : S.Leaf)
    (T : KernelTower Ω n) (f : FinitePath Ω n → ℝ) :
    (S.sampleLaw T).expect (fun x => f (S.pathAt a x)) = (KernelTower.law n T).expect f := by
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.KernelTower.law
theorem OAI.DilutedSpinGlass.PrescribedTree.anchor_centered_bound line 39
Source documentation
The anchor-marginal argument in pert:score-identity, before root averaging. It uses the actual old-tree joint law, not independent replicas.
```
theorem anchor_centered_bound {n : ℕ} (S : PrescribedTree n) (a : S.Leaf)
    (T : KernelTower Ω n) (f : Sample Ω S → ℝ) (g : FinitePath Ω n → ℝ)
    {B center : ℝ} (hB : 0 ≤ B) (hf : ∀ x, |f x| ≤ B) :
    |(S.sampleLaw T).expect (fun x => f x * g (S.pathAt a x)) -
      (S.sampleLaw T).expect f * center| ≤
      B * (KernelTower.law n T).expect (fun y => |g y-center|) := by
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.KernelTower.law