StemTwoSideProjection.lean`

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.DilutedSpinGlass.FiniteLaw.pairProjectionSq_le_of_contractions line 13
Source documentation
Pairwise projection retains both sampled vectors and their correlation with any later old test. Only the separate sides are independent.
```
theorem pairProjectionSq_le_of_contractions (P : FiniteLaw Ω) (X Y : Ω → Fin N → ℝ)
    (hX : ∀ x i, |X x i|≤1) (hY : ∀ x i, |Y x i|≤1) (A : ℝ)
    (hA : ∀ B : Fin N → ℝ, (∀ i, |B i|≤1) →
      P.expect (fun x => (dot (fun i => X x i-Y x i) B)^2) ≤ A) :
    pairProjectionSq P X Y ≤ 4*A := by
…
```
Mentions: OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.FiniteLaw.dot, OAI.DilutedSpinGlass.FiniteLaw.pairProjectionSq
theorem OAI.DilutedSpinGlass.PrescribedTree.stem_node_two_side_projection_sq line 46
Source documentation
The complete two-sided projection at a prescribed later first split. Both products and both projected means use the same original sampled paths. The right side contains genuine proper-child covariance energies only.
```
theorem stem_node_two_side_projection_sq (k : ℕ+) (C : Fin k → PrescribedTree n)
    (a : (PrescribedTree.node k C).Leaf) (r : ℕ)
    (T : KernelTower Ω (n+1+r)) (f : FinitePath Ω (n+1+r) → Fin N → ℝ)
    (hf : ∀ x i, |f x i|≤1) :
    let S := PrescribedTree.node k C
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath
theorem OAI.DilutedSpinGlass.PrescribedTree.stem_node_two_side_projection_l2 line 64
Source documentation
Same error in L2, allowing arbitrary bounded correlated old scalar tests by Cauchy--Schwarz in the subsequent shifted-matrix identity.
```
theorem stem_node_two_side_projection_l2 (k : ℕ+) (C : Fin k → PrescribedTree n)
    (a : (PrescribedTree.node k C).Leaf) (r : ℕ)
    (T : KernelTower Ω (n+1+r)) (f : FinitePath Ω (n+1+r) → Fin N → ℝ)
    (hf : ∀ x i, |f x i|≤1) :
    let S := PrescribedTree.node k C
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath