OAI/Probability/DilutedSpin/ShapeMatrixPhysical.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DilutedSpinGlass.UniversalDictionary.rootMatrixObservable line 23

   Source documentation

   A matrix multioverlap at the actual heterogeneous physical root, retaining the literal old-test transport and root-dependent alphabet.

   noncomputable def rootMatrixObservable (z : FullRootState Y X (Labels L (Site N)) M) : ℝ :=
   …

   Mentions: OAI.DilutedSpinGlass.FullRootState, OAI.DilutedSpinGlass.UniversalDictionary.Labels

2. lemma OAI.DilutedSpinGlass.UniversalDictionary.integral_rootShapeHistory_matrix line 31
3. lemma OAI.DilutedSpinGlass.UniversalDictionary.integrable_rootShapeHistory_general line 48
4. lemma OAI.DilutedSpinGlass.UniversalDictionary.shapeAverage_matrix line 72
5. lemma OAI.DilutedSpinGlass.UniversalDictionary.shapeCovariance_matrix line 82