PhysicalTreeMatrix.lean`

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DilutedSpinGlass.UniversalDictionary.physicalTreeMatrixCovariance line 16
Source documentation
Literal centered history for the multileaf old overlap, with the actual variable-marker root alphabet.
```
noncomputable def physicalTreeMatrixCovariance (m : Fin (L+1) → ℝ)
    (S : PrescribedTree (L+1)) (a : S.Leaf) (M : Model p) (C H : ℝ)
    (N : ℕ) (u : Spec L×ℕ → ℝ) (T : PrescribedTree (L+1)) (q : Option (Fin k) → T.Leaf) : ℝ :=
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.Model, OAI.DilutedSpinGlass.UniversalDictionary.Spec, OAI.DilutedSpinGlass.q
lemma OAI.DilutedSpinGlass.UniversalDictionary.physicalTreeMatrixCovariance_eq line 32
lemma OAI.DilutedSpinGlass.UniversalDictionary.physicalTreeMatrixCovariance_history line 47
Source documentation
The canonical insertion history really has the precise head/tail required by the integrated proper-child inequality.
```
lemma physicalTreeMatrixCovariance_history (m : Fin (L+1) → ℝ)
    (S : PrescribedTree (L+1)) (a : S.Leaf) (M : Model p) (C H : ℝ)
    (N : ℕ) (u : Spec L×ℕ → ℝ) (T : PrescribedTree (L+1)) (q : Option (Fin (k+1)) → T.Leaf) :
    physicalTreeMatrixCovariance m S a M C H N u T q =
      matrixRootCovariance
        (fullRootLaw (fun _ : Fin N => M.field.toMeasure) (bondLaw M N)
          (markLaw (weights L) N) (M.alpha*N) (scoreRate N))
        (rootAlphabet (Ω := Fin N → Spin) (A := fun i : Labels L (Site N) => Alphabet i.1.1)) T S q
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.Model, OAI.DilutedSpinGlass.UniversalDictionary.Spec, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.UniversalDictionary.physicalTreeMatrixCovariance, OAI.DilutedSpinGlass.fullRootLaw, OAI.DilutedSpinGlass.UniversalDictionary.weights, OAI.DilutedSpinGlass.scoreRate, OAI.DilutedSpinGlass.Spin, OAI.DilutedSpinGlass.UniversalDictionary.Labels, OAI.DilutedSpinGlass.UniversalDictionary.Alphabet