ShapeMatrix.lean`

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DilutedSpinGlass.PrescribedTree.matrixSplitTest line 14
def OAI.DilutedSpinGlass.PrescribedTree.spatialProduct line 17
lemma OAI.DilutedSpinGlass.PrescribedTree.spatialProduct_bound line 21
lemma OAI.DilutedSpinGlass.PrescribedTree.matrixObservableHistory_sum line 38
lemma OAI.DilutedSpinGlass.PrescribedTree.matrixObservableHistory_div line 53
lemma OAI.DilutedSpinGlass.PrescribedTree.shapeHistory_matrix line 68
theorem OAI.DilutedSpinGlass.PrescribedTree.matrix_history_spatialProduct line 84
Source documentation
Empirical multioverlap and literal full-matrix history commute with the single shared site average. Old tests may depend on every old sample.
```
theorem matrix_history_spatialProduct (T : PrescribedTree (L+1)) (q : Option (Fin k) → T.Leaf)
    (K : KernelTower Ω (L+1)) (m : Fin (L+2) → ℝ)
    (D : Option (Fin k) → FinitePath Ω (L+1) → Fin N → ℝ)
    (S : PrescribedTree (L+1)) (a : S.Leaf) (f : Sample Ω S → ℝ) :
    matrixObservableHistory T q K m
      (List.ofFn (fun j : Fin k => (some j : Option (Fin k)))).reverse S a (spatialProduct D) f =
      (∑ i : Fin N, shapeHistory K m (matrixSplitTest T q) (fun c x => D c x i) S a f)/(N:ℝ) := by
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.PrescribedTree.matrixObservableHistory, OAI.DilutedSpinGlass.PrescribedTree.spatialProduct, OAI.DilutedSpinGlass.PrescribedTree.shapeHistory, OAI.DilutedSpinGlass.PrescribedTree.matrixSplitTest
lemma OAI.DilutedSpinGlass.PrescribedTree.matrix_history_spatialProduct_same line 95