CavityFiniteGroupSelection.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Selecting the assigned special axes from the Gaussian spectral-group block gives precisely the finite cavity field law.

def OAI.InvariantIsing.cavityFiniteReplicaSpectralBlock line 16
def OAI.InvariantIsing.cavitySelectedGroupIndex line 23
lemma OAI.InvariantIsing.cavity_finite_group_covariance_posSemidef line 27
lemma OAI.InvariantIsing.cavity_selected_group_covariance line 60

theorem OAI.InvariantIsing.cavity_selected_group_gaussian_law line 90

Source documentation

The physical selected coordinates have exactly the covariance of root-plus-forest cavity replicas. Unselected axes integrate out.

theorem cavity_selected_group_gaussian_law {m d n r k : ℕ}
    (rho lam : Fin m → ℝ) (hrho : ∀ a, 0 < rho a) (hsum : ∑ a, rho a = 1)
    (g : Fin d → Fin m) (e : Fin d → Fin m × Fin k)
    (he : Function.Injective e) (heg : ∀ a, (e a).1 = g a)
    (p : OverlapPath) (q : Fin (n + 1) → ℝ) (hq : Monotone q)
    (σ : Fin r → LabeledLeaf n) :
    (multivariateGaussian (0 : EuclideanSpace ℝ (Fin m × (Fin r × Fin k)))
      (cavityGroupBlockCovariance k rho
        (cavityFiniteReplicaSpectralBlock rho lam hrho hsum p q σ))).map
      (cavityGaussianCoordinateMap (cavitySelectedGroupIndex e)) =
      multivariateGaussian 0 (cavityFiniteCanonicalReplicaCovariance rho lam hrho hsum g p q σ) := by
…

Mentions: OAI.InvariantIsing.OverlapPath, OAI.InvariantIsing.cavityGroupBlockCovariance, OAI.InvariantIsing.cavityFiniteReplicaSpectralBlock, OAI.InvariantIsing.cavityGaussianCoordinateMap, OAI.InvariantIsing.cavitySelectedGroupIndex, OAI.InvariantIsing.cavityFiniteCanonicalReplicaCovariance