CavityGroupCovariance.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Covariance identification for the joint spectral-group projection. Off-group and off-axis covariances vanish, while replica covariances are the normalized Gram matrices in each eigenspace.

lemma OAI.InvariantIsing.cavityGroupProjectionMatrix_covariance line 15
def OAI.InvariantIsing.cavityGroupReplicaCovariance line 46
lemma OAI.InvariantIsing.cavityGroupProjection_covariance_tendsto line 51

theorem OAI.InvariantIsing.cavityGroupFrameProjection_tendsto_of_replicaGram line 73

Source documentation

All spectral groups converge jointly to the Gaussian array prescribed by their replica Gram limits, including singular limiting arrays.

theorem cavityGroupFrameProjection_tendsto_of_replicaGram {m r q : ℕ}
    (N : ℕ → Fin m → ℕ) (hN : ∀ a, Tendsto (fun k => N k a) atTop atTop)
    (v : (k : ℕ) → (a : Fin m) → Fin r → Fin (N k a) → ℝ)
    (Q : Fin m → Matrix (Fin r) (Fin r) ℝ)
    (hQ : Tendsto (fun k a i j => (∑ l, v k a i l * v k a j l) / (N k a : ℝ))
      atTop (𝓝 Q)) :
    TendstoInDistribution (fun k => cavityGroupFrameProjection (q := q) (v k)) atTop id
…

Mentions: OAI.InvariantIsing.cavityGroupFrameProjection