OAI/Probability/DilutedSpin/AnchorExtension.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DilutedSpinGlass.PrescribedTree.hasDerivAt_protected_expect_varying line 13

   Source documentation

   A parameter-dependent old test can be differentiated without changing any of the actual tree sampling kernels.

   theorem hasDerivAt_protected_expect_varying {n : ℕ} (S : PrescribedTree n)
       (T : KernelTower Ω n) (m : Fin (n+1) → ℝ)
       (hm : ∀ j : Fin n, m j.succ ≠ 0) (hroot : m 0 = 0)
       (C : Finset (Leaf S)) {G : ℝ → Sample Ω S → ℝ} {G' : Sample Ω S → ℝ}
       {f : ℝ → FinitePath Ω n → ℝ} {f' : FinitePath Ω n → ℝ} {u : ℝ}
       (hf : ∀ y, HasDerivAt (fun t => f t y) (f' y) u)
       (hG : ∀ x, HasDerivAt (fun t => G t x) (G' x) u) :
       HasDerivAt (fun t => (sampleLaw S (KernelTower.tilt n T (fun j => m j.succ) (f t))).expect
         (fun x => G t x * Real.exp (-protectedLog S C (f t) x)))
         ((sampleLaw S (KernelTower.tilt n T (fun j => m j.succ) (f u))).expect
           (fun x => G' x * Real.exp (-protectedLog S C (f u) x)) +
          (sampleLaw S (KernelTower.tilt n T (fun j => m j.succ) (f u))).expect
   …

   Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.sampleLaw, OAI.DilutedSpinGlass.KernelTower.tilt, OAI.DilutedSpinGlass.PrescribedTree.protectedLog

2. theorem OAI.DilutedSpinGlass.PrescribedTree.hasDerivAt_fullyProtected_varying line 40

   Source documentation

   The full cancellation calculus, with a moving test. Fresh branches are sampled genuinely, not defined by their expectation.

   theorem hasDerivAt_fullyProtected_varying {n : ℕ} (S : PrescribedTree n)
       (T : KernelTower Ω n) (m : Fin (n+1) → ℝ)
       (hm : ∀ j : Fin n, m j.succ ≠ 0) (hroot : m 0 = 0) (hend : m (Fin.last n) = 1)
       (D : FinitePath Ω n → ℝ) {G : ℝ → Sample Ω S → ℝ} {G' : Sample Ω S → ℝ} (u : ℝ)
       (hu : ∀ y, 0 < 1+u*D y) (hG : ∀ x, HasDerivAt (fun t => G t x) (G' x) u) :
       HasDerivAt (fun t => fullyProtected S T m D (G t) t)
         (fullyProtected S T m D G' u +
          ∑ v : Internal S, gamma S m v *
           fullyProtected (grow S v) T m D (fun x => G u (oldSample S v x) * D (newPath S v x)) u) u := by
   …

   Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.PrescribedTree.fullyProtected, OAI.DilutedSpinGlass.PrescribedTree.Internal, OAI.DilutedSpinGlass.PrescribedTree.gamma, OAI.DilutedSpinGlass.PrescribedTree.grow, OAI.DilutedSpinGlass.PrescribedTree.oldSample, OAI.DilutedSpinGlass.PrescribedTree.newPath

3. def OAI.DilutedSpinGlass.PrescribedTree.anchorEval line 73

   Source documentation

   Unused old positions are a finite family of genuine path projections. In a canceled-anchor application these are all old leaves except the anchor. Every already selected color is canceled.

   noncomputable def anchorEval {n : ℕ} (S : PrescribedTree n)
       (T : KernelTower Ω n) (m : Fin (n+1) → ℝ) (D : FinitePath Ω n → ℝ)
       {ι : Type} (A : Finset ι) (U : ι → Sample Ω S → FinitePath Ω n)
       (G : Sample Ω S → ℝ) (t : ℝ) : ℝ :=
   …

   Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.Sample

4. theorem OAI.DilutedSpinGlass.PrescribedTree.fullyProtected_sum line 79
5. theorem OAI.DilutedSpinGlass.PrescribedTree.hasDerivAt_anchorEval line 88
6. def OAI.DilutedSpinGlass.PrescribedTree.anchorIterate line 126

   Source documentation

   Ordered histories for all orders of the canceled-anchor expansion. The state records precisely which OLD positions remain eligible.

   noncomputable def anchorIterate {n : ℕ} (T : KernelTower Ω n) (m : Fin (n+1) → ℝ)
       (D : FinitePath Ω n → ℝ) {ι : Type} [DecidableEq ι] :
       ℕ → (S : PrescribedTree n) → (A : Finset ι) →
         (ι → Sample Ω S → FinitePath Ω n) → (Sample Ω S → ℝ) → ℝ → ℝ
     | 0, S, A, U, G, t => anchorEval S T m D A U G t
     | k+1, S, A, U, G, t =>
         (∑ i ∈ A, anchorIterate T m D k S (A.erase i) U (fun x => G x * D (U i x)) t) +
         ∑ v : Internal S, gamma S m v * anchorIterate T m D k (grow S v) A
           (fun i x => U i (oldSample S v x))
           (fun x => G (oldSample S v x) * D (newPath S v x)) t
   
   /-- Every derivative order of the actual finite-kernel canceled-anchor

   Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.PrescribedTree.anchorEval, OAI.DilutedSpinGlass.PrescribedTree.Internal, OAI.DilutedSpinGlass.PrescribedTree.gamma, OAI.DilutedSpinGlass.PrescribedTree.grow, OAI.DilutedSpinGlass.PrescribedTree.oldSample, OAI.DilutedSpinGlass.PrescribedTree.newPath

7. theorem OAI.DilutedSpinGlass.PrescribedTree.hasDerivAt_anchorIterate line 139

   Source documentation

   Every derivative order of the actual finite-kernel canceled-anchor expectation is the ordered old-or-fresh extension sum.

   theorem hasDerivAt_anchorIterate {n : ℕ} (T : KernelTower Ω n) (m : Fin (n+1) → ℝ)
       (hm : ∀ j : Fin n, m j.succ ≠ 0) (hroot : m 0 = 0) (hend : m (Fin.last n) = 1)
       (D : FinitePath Ω n → ℝ) {ι : Type} [DecidableEq ι]
       (k : ℕ) (S : PrescribedTree n) (A : Finset ι)
       (U : ι → Sample Ω S → FinitePath Ω n) (G : Sample Ω S → ℝ)
       (u : ℝ) (hu : ∀ y, 0 < 1+u*D y) :
       HasDerivAt (anchorIterate T m D k S A U G)
         (anchorIterate T m D (k+1) S A U G u) u := by
   …

   Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.PrescribedTree.anchorIterate

8. theorem OAI.DilutedSpinGlass.FiniteLaw.tilt_const line 164
9. theorem OAI.DilutedSpinGlass.KernelTower.tilt_const line 173
10. theorem OAI.DilutedSpinGlass.PrescribedTree.leafSum_mono line 191
11. theorem OAI.DilutedSpinGlass.PrescribedTree.fullyProtected_zero line 196
12. theorem OAI.DilutedSpinGlass.PrescribedTree.anchorEval_zero line 202
13. theorem OAI.DilutedSpinGlass.PrescribedTree.protected_density_bound line 212

    Source documentation

    The denominator in the protected tree rule is uniformly bounded on a fixed real neighborhood of zero, independently of all kernels and depth.

    theorem protected_density_bound {n : ℕ} (S : PrescribedTree n)
        (D : FinitePath Ω n → ℝ) (hD : ∀ y, |D y| ≤ 1)
        {t : ℝ} (ht : |t| ≤ 1/2) (x : Sample Ω S) :
        Real.exp (-leafSum S (fun y => Real.log (1+t*D y)) x) ≤ (2:ℝ) ^ leaves S := by
    …

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.PrescribedTree.leafSum, OAI.DilutedSpinGlass.PrescribedTree.leaves

14. theorem OAI.DilutedSpinGlass.PrescribedTree.abs_fullyProtected_le line 233
15. theorem OAI.DilutedSpinGlass.PrescribedTree.abs_anchorEval_le line 243
16. def OAI.DilutedSpinGlass.PrescribedTree.derivativeBound line 273

    Source documentation

    A depth-independent bound on derivative order k; the total absolute one-step extension coefficient is the count of eligible old positions plus all sampled leaves.

    noncomputable def derivativeBound : ℕ → ℕ → ℝ
      | q, 0 => (2:ℝ)^q
      | q, k+1 => (q:ℝ) * derivativeBound (q+1) k

    Mentions: OAI.DilutedSpinGlass.q

17. theorem OAI.DilutedSpinGlass.PrescribedTree.derivativeBound_nonneg line 277
18. theorem OAI.DilutedSpinGlass.PrescribedTree.derivativeBound_mono line 282
19. theorem OAI.DilutedSpinGlass.PrescribedTree.abs_anchorIterate_le line 294

    Source documentation

    Uniform real control of the full OLD-or-FRESH derivative expansion. No depth, number of kernel states, or base-disorder law enters the bound.

    theorem abs_anchorIterate_le {n : ℕ} (T : KernelTower Ω n) (m : Fin (n+1) → ℝ)
        (hm : Monotone m) (hpos : ∀ j, 0 ≤ m j) (hroot : m 0 = 0)
        (hend : m (Fin.last n) = 1) (D : FinitePath Ω n → ℝ) (hD : ∀ y, |D y| ≤ 1)
        {ι : Type} [DecidableEq ι] (k : ℕ) (S : PrescribedTree n) (A : Finset ι)
        (U : ι → Sample Ω S → FinitePath Ω n) (G : Sample Ω S → ℝ)
        {B t : ℝ} (hB : 0 ≤ B) (hG : ∀ x, |G x| ≤ B) (ht : |t| ≤ 1/2) :
        |anchorIterate T m D k S A U G t| ≤ B * derivativeBound (leaves S + A.card) k := by
    …

    Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.PrescribedTree.anchorIterate, OAI.DilutedSpinGlass.PrescribedTree.derivativeBound, OAI.DilutedSpinGlass.PrescribedTree.leaves

20. theorem OAI.DilutedSpinGlass.PrescribedTree.card_leaf line 355
21. instance OAI.DilutedSpinGlass.PrescribedTree.leafDecidableEq line 364
22. theorem OAI.DilutedSpinGlass.PrescribedTree.abs_freshEval_le line 369
23. theorem OAI.DilutedSpinGlass.PrescribedTree.abs_vertexScore_le line 380
24. theorem OAI.DilutedSpinGlass.PrescribedTree.exp_neg_leafSum_log line 407
25. def OAI.DilutedSpinGlass.PrescribedTree.anchorInsertion line 417

    Source documentation

    The actual anchor expectation in pert:palm-expression, with the prior kernels updated by the new insertion. G includes the numerator score mark.

    noncomputable def anchorInsertion {n : ℕ} (S : PrescribedTree n)
        (T : KernelTower Ω n) (m : Fin (n+1) → ℝ) (a : Leaf S)
        (G : Sample Ω S → ℝ) (A : FinitePath Ω n → ℝ) : ℝ :=
    …

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.FinitePath

26. theorem OAI.DilutedSpinGlass.PrescribedTree.anchorEval_eq_anchorInsertion line 425

    Source documentation

    Links the proved ordered history derivative rule to the single canceled anchor of the manuscript, not a different protected-leaf functional.

    theorem anchorEval_eq_anchorInsertion {n : ℕ} (S : PrescribedTree n)
        (T : KernelTower Ω n) (m : Fin (n+1) → ℝ) (D : FinitePath Ω n → ℝ)
        (a : Leaf S) (G : Sample Ω S → ℝ) (t : ℝ) (ht : ∀ y, 0 < 1+t*D y) :
        anchorEval S T m D (Finset.univ.erase a) (pathAt S) G t =
          anchorInsertion S T m a G (fun y => 1+t*D y) := by
    …

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.PrescribedTree.anchorEval, OAI.DilutedSpinGlass.PrescribedTree.pathAt, OAI.DilutedSpinGlass.PrescribedTree.anchorInsertion

27. def OAI.DilutedSpinGlass.PrescribedTree.anchorDerivative line 448

    Source documentation

    The derivative of a canceled-anchor insertion, retaining the actual tree score and the correction from the canceled denominator.

    noncomputable def anchorDerivative {n : ℕ} (S : PrescribedTree n)
        (T : KernelTower Ω n) (m : Fin (n+1) → ℝ) (a : Leaf S)
        (G : Sample Ω S → ℝ) (A E : FinitePath Ω n → ℝ) : ℝ :=
    …

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.FinitePath

28. theorem OAI.DilutedSpinGlass.PrescribedTree.hasDerivAt_anchorInsertion line 456
29. theorem OAI.DilutedSpinGlass.PrescribedTree.abs_div_bound line 477
30. theorem OAI.DilutedSpinGlass.PrescribedTree.abs_anchorDerivative_le line 485

    Source documentation

    Uniform bound in the auxiliary u direction. It uses only probability normalization and the telescoping absolute tree coefficients.

    theorem abs_anchorDerivative_le {n : ℕ} (S : PrescribedTree n)
        (T : KernelTower Ω n) (m : Fin (n+1) → ℝ)
        (hm : Monotone m) (hpos : ∀ j, 0 ≤ m j) (hroot : m 0 = 0)
        (hend : m (Fin.last n) = 1) (a : Leaf S) (G : Sample Ω S → ℝ)
        (A E : FinitePath Ω n → ℝ) {B : ℝ} (hB : 0 ≤ B)
        (hG : ∀ x, |G x| ≤ B) (hA : ∀ y, (1:ℝ)/2 ≤ A y) (hE : ∀ y, |E y| ≤ 1) :
        |anchorDerivative S T m a G A E| ≤ (4+8*(leaves S:ℝ))*B := by
    …

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.anchorDerivative, OAI.DilutedSpinGlass.PrescribedTree.leaves

31. theorem OAI.DilutedSpinGlass.PrescribedTree.affine_two_lower_half line 505
32. theorem OAI.DilutedSpinGlass.PrescribedTree.anchorInsertion_sub_le line 519

    Source documentation

    The u-error in pert:analytic is uniformly linear, before any root averaging. No analyticity or enlargement of computational limits is needed.

    theorem anchorInsertion_sub_le {n : ℕ} (S : PrescribedTree n)
        (T : KernelTower Ω n) (m : Fin (n+1) → ℝ)
        (hm : ∀ j : Fin n, m j.succ ≠ 0) (hmono : Monotone m) (hpos : ∀ j, 0 ≤ m j)
        (hroot : m 0 = 0) (hend : m (Fin.last n) = 1)
        (a : Leaf S) (G : Sample Ω S → ℝ) (D E : FinitePath Ω n → ℝ)
        {B t u : ℝ} (hB : 0 ≤ B) (hG : ∀ x, |G x| ≤ B)
        (hD : ∀ y, |D y| ≤ 1) (hE : ∀ y, |E y| ≤ 1)
        (ht : |t| ≤ 1/4) (huz : 0 ≤ u) (hu : u ≤ 1/4) :
        |anchorInsertion S T m a G (fun y => 1+t*D y+u*E y) -
          anchorInsertion S T m a G (fun y => 1+t*D y)| ≤ (4+8*(leaves S:ℝ))*B*u := by
    …

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.anchorInsertion, OAI.DilutedSpinGlass.PrescribedTree.leaves

33. theorem OAI.DilutedSpinGlass.jet_iteratedDerivWithin line 557

    Source documentation

    Identifies an explicitly constructed differential jet with Mathlib's iterated derivatives, without any analytic or compactness assumption.

    theorem jet_iteratedDerivWithin {F : ℕ → ℝ → ℝ} {s : Set ℝ}
        (hs : UniqueDiffOn ℝ s)
        (hF : ∀ k x, x ∈ s → HasDerivAt (F k) (F (k+1) x) x)
        (k : ℕ) : EqOn (iteratedDerivWithin k (F 0) s) (F k) s := by
    …

34. theorem OAI.DilutedSpinGlass.jet_contDiffOn line 568
35. theorem OAI.DilutedSpinGlass.jet_taylor_bound line 583

    Source documentation

    Uniform finite Taylor remainder for the explicit jet used in the canceled-anchor identities. Only a bound on the required derivative enters.

    theorem jet_taylor_bound {F : ℕ → ℝ → ℝ} {a b t C : ℝ} (hab : a < b)
        (hF : ∀ k x, x ∈ Icc a b → HasDerivAt (F k) (F (k+1) x) x)
        (k : ℕ) (ht : t ∈ Icc a b)
        (hC : ∀ x ∈ Icc a b, |F (k+1) x| ≤ C) :
        |F 0 t - ∑ j ∈ Finset.range (k+1), F j a / (j.factorial:ℝ) * (t-a)^j| ≤
          C * (t-a)^(k+1) / (k.factorial:ℝ) := by
    …

36. def OAI.DilutedSpinGlass.PrescribedTree.anchorCoefficient line 612

    Source documentation

    The literal ordered-history Taylor coefficient of the single anchor. Only the anchor is initially protected.

    noncomputable def anchorCoefficient {n : ℕ} (S : PrescribedTree n)
        (T : KernelTower Ω n) (m : Fin (n+1) → ℝ) (D : FinitePath Ω n → ℝ)
        (a : Leaf S) (G : Sample Ω S → ℝ) (k : ℕ) : ℝ :=
    …

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.PrescribedTree.Sample

37. theorem OAI.DilutedSpinGlass.PrescribedTree.anchorInsertion_taylor_bound line 620

    Source documentation

    Quantitative real Taylor expansion of the actual canceled-anchor insertion. This is uniform in every probability kernel and can therefore be root-averaged before selecting any subsequence.

    theorem anchorInsertion_taylor_bound {n : ℕ} (S : PrescribedTree n)
        (T : KernelTower Ω n) (m : Fin (n+1) → ℝ)
        (hm : ∀ j : Fin n, m j.succ ≠ 0) (hmono : Monotone m) (hpos : ∀ j, 0 ≤ m j)
        (hroot : m 0 = 0) (hend : m (Fin.last n) = 1)
        (D : FinitePath Ω n → ℝ) (hD : ∀ y, |D y| ≤ 1)
        (a : Leaf S) (G : Sample Ω S → ℝ) {B t : ℝ}
        (hB : 0 ≤ B) (hG : ∀ x, |G x| ≤ B) (ht : t ∈ Set.Icc (0:ℝ) (1/2)) (k : ℕ) :
        |anchorInsertion S T m a G (fun y => 1+t*D y) -
          ∑ j ∈ Finset.range (k+1), anchorCoefficient S T m D a G j * t^j| ≤
            (B * derivativeBound (leaves S + (Finset.univ.erase a).card) (k+1) /
              (k.factorial:ℝ)) * t^(k+1) := by
    …

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.PrescribedTree.anchorInsertion, OAI.DilutedSpinGlass.PrescribedTree.anchorCoefficient, OAI.DilutedSpinGlass.PrescribedTree.derivativeBound, OAI.DilutedSpinGlass.PrescribedTree.leaves

38. def OAI.DilutedSpinGlass.PrescribedTree.sampleFst line 667
39. def OAI.DilutedSpinGlass.PrescribedTree.sampleSnd line 671
40. def OAI.DilutedSpinGlass.PrescribedTree.samplePair line 675
41. lemma OAI.DilutedSpinGlass.PrescribedTree.sampleFst_pair line 679
42. lemma OAI.DilutedSpinGlass.PrescribedTree.sampleSnd_pair line 688
43. lemma OAI.DilutedSpinGlass.PrescribedTree.samplePair_projections line 697
44. def OAI.DilutedSpinGlass.PrescribedTree.sampleProdEquiv line 707
45. lemma OAI.DilutedSpinGlass.PrescribedTree.pathAt_sampleFst line 713
46. lemma OAI.DilutedSpinGlass.PrescribedTree.pathAt_sampleSnd line 719
47. lemma OAI.DilutedSpinGlass.PrescribedTree.sampleLaw_prod_weight line 727
48. lemma OAI.DilutedSpinGlass.PrescribedTree.sampleExpect_prod line 746

    Source documentation

    Fresh mark samples are genuinely independent of every old physical/mark sample in a prescribed tree, not merely of a single replica.

    lemma sampleExpect_prod {n : ℕ} (S : PrescribedTree n)
        (T : KernelTower Ω n) (U : KernelTower Λ n) (f : Sample (Ω × Λ) S → ℝ) :
        (S.sampleLaw (KernelTower.prod n T U)).expect f =
          (S.sampleLaw T).expect (fun x => (S.sampleLaw U).expect (fun y => f (samplePair S x y))) := by
    …

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.KernelTower.prod, OAI.DilutedSpinGlass.PrescribedTree.samplePair

49. lemma OAI.DilutedSpinGlass.PrescribedTree.expect_prod_separated line 764