TwoSideProjection.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.DilutedSpinGlass.PrescribedTree.node_two_side_projection line 13
Source documentation
The two-sided projection error at the first branching vertex, with both copies sampled independently from the full genuine prescribed-tree law.
```
theorem node_two_side_projection (k : ℕ+) (C : Fin k → PrescribedTree n)
    (T : KernelTower Ω (n+1)) (f : FinitePath Ω (n+1) → Fin N → ℝ)
    (hf : ∀ x v, |f x v| ≤ 1) :
    let S := PrescribedTree.node k C
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath
theorem OAI.DilutedSpinGlass.PrescribedTree.node_two_side_projection_test line 56
Source documentation
The squared contraction error permits arbitrary bounded old scalar multipliers through Cauchy--Schwarz; no independence of that test is used.
```
theorem node_two_side_projection_test (k : ℕ+) (C : Fin k → PrescribedTree n)
    (T : KernelTower Ω (n+1)) (f : FinitePath Ω (n+1) → Fin N → ℝ)
    (hf : ∀ x v, |f x v| ≤ 1)
    (g : Sample Ω (.node k C) × Sample Ω (.node k C) → ℝ) (hg : ∀ z, |g z| ≤ 1) :
    let S := PrescribedTree.node k C
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.Sample