GeneralPairSquare.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.DilutedSpinGlass.PrescribedTree.pair_square_identity_general line 17

Source documentation

The exact nonnegative-square identity before root averaging. It follows from actual two-path marginals and complete old-law projectivity.

theorem pair_square_identity_general (T : KernelTower Ω n) (m : Fin (n+1) → ℝ)
    (hend : m (Fin.last n) = 1) (S : PrescribedTree n) (a b : S.Leaf)
    (d : ℕ) (hd : d < n) (hsplit : splitDepth S a b = d)
    (R : FinitePath Ω n → FinitePath Ω n → ℝ)
    (hOld : ∀ c, splitDepth S a c = d → ∀ x : Sample Ω S,
      R (S.pathAt a x) (S.pathAt c x) = R (S.pathAt a x) (S.pathAt b x)) :
    (1/2:ℝ) * ∑ v : S.Internal, pairFreshCost S m a d v *
      ((grow S v).sampleLaw T).expect (fun x =>
        (R (S.pathAt a (oldSample S v x)) (S.pathAt b (oldSample S v x)) -
          R ((grow S v).pathAt (oldLeaf S v a) x) ((grow S v).pathAt (newLeaf S v) x))^2) =
      (m ⟨d+1,by omega⟩-m ⟨d,by omega⟩) *
        (S.sampleLaw T).expect (fun x => R (S.pathAt a x) (S.pathAt b x)^2) +
…

lemma OAI.DilutedSpinGlass.PrescribedTree.fork_two_positions line 119
theorem OAI.DilutedSpinGlass.PrescribedTree.singleton_decorrelation_bound line 130