OAI/Probability/DilutedSpin/MarkerPhysicalBridge.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DilutedSpinGlass.UniversalDictionary.rootMarkerObservable line 21

   Source documentation

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

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

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

2. lemma OAI.DilutedSpinGlass.UniversalDictionary.integral_rootShapeHistory_marker line 29
3. lemma OAI.DilutedSpinGlass.UniversalDictionary.shapeAverage_marker line 46
4. lemma OAI.DilutedSpinGlass.UniversalDictionary.shapeCovariance_marker line 56