UniformRootDecorrelation.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DilutedSpinGlass.PrescribedTree.pairRootMean line 17
def OAI.DilutedSpinGlass.PrescribedTree.pairRootCovariance line 21
lemma OAI.DilutedSpinGlass.PrescribedTree.pairRootCovariance_center line 30

theorem OAI.DilutedSpinGlass.PrescribedTree.root_decorrelation_bound line 54

Source documentation

The single-copy conditional covariance estimate with the exact shared root covariance. Applicability is to arbitrary old trees, not surrogate laws.

theorem root_decorrelation_bound (hd : d < n) (hab : splitDepth S a b = d)
    (v : S.Internal) (hav : freshSplitDepth S v a = d) (hbv : freshSplitDepth S v b = d)
    (hm : Monotone m) (hp : ∀ j, 0 ≤ m j) (hend : m (Fin.last n) = 1)
    (hX : ∀ z x i, |X z x i| ≤ 1)
    (hOld : ∀ z c, splitDepth S a c = d → ∀ x : Sample (Ω z) S,
      X z (S.pathAt c x) = X z (S.pathAt b x))
    (hE : Integrable (fun z => KernelTower.prefixEnergyAt n (T z) d (X z)) μ)
    (hA : Integrable (fun z => (S.sampleLaw (T z)).expect (fun x =>
      FiniteLaw.dot (X z (S.pathAt a x)) (X z (S.pathAt b x))^2)) μ)
    (hH : Integrable (fun z => pairObservableHistory (T z) m S a d
      (fun x y => FiniteLaw.dot (X z x) (X z y))
      (fun x => FiniteLaw.dot (X z (S.pathAt a x)) (X z (S.pathAt b x)))) μ) :
…

Mentions: OAI.DilutedSpinGlass.PrescribedTree.splitDepth, OAI.DilutedSpinGlass.PrescribedTree.freshSplitDepth, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.KernelTower.prefixEnergyAt, OAI.DilutedSpinGlass.FiniteLaw.dot, OAI.DilutedSpinGlass.PrescribedTree.pairObservableHistory

lemma OAI.DilutedSpinGlass.PrescribedTree.pairHistoryMass_grid line 103
Source documentation
Unlike a bound by all grid vertices, the exact full history mass is uniform in the number of unary levels.
```
lemma pairHistoryMass_grid (hL : 0<L) (S : PrescribedTree L) (a : S.Leaf) :
    pairHistoryMass S (grid L 0 L) a=2*(leaves S:ℝ)-1 := by
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.pairHistoryMass, OAI.DilutedSpinGlass.PrescribedTree.grid, OAI.DilutedSpinGlass.PrescribedTree.leaves