OAI/Probability/DilutedSpin/CommonFresh.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.rootExternalTreeScore_probe line 30

   Source documentation

   Changing only the fresh probe label does not change its alphabet, prior, or observable. All old labels, factors, and counts remain literally fixed.

   lemma rootExternalTreeScore_probe (q : K) (j k : ℕ) (z : FullRootState Y X ((K×ℕ)×Z) M)
       (v : Z) (t u : ℝ) :
       rootExternalTreeScore S a T (fun i => Q i.1.1) (fun l => m l.succ) base old
         (fun i x y => 1+t*D i.1.1 i.2 x y+u*E i.1.1 i.2 x y)
         (fun i => E i.1.1 i.2) f z ((q,j),v) =
       rootExternalTreeScore S a T (fun i => Q i.1.1) (fun l => m l.succ) base old
         (fun i x y => 1+t*D i.1.1 i.2 x y+u*E i.1.1 i.2 x y)
         (fun i => E i.1.1 i.2) f z ((q,k),v) := rfl

   Mentions: OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.FullRootState, OAI.DilutedSpinGlass.HeterogeneousMarks.rootExternalTreeScore

2. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.externalAverage_probe line 39
3. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.externalCovariance_probe line 60