OAI/Probability/InvariantIsing/Cavity/CavityFiniteReplicaLaw.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The exact Gaussian law used on the finite spectral side of the physical replica comparison, with every covariance fixed by the overlap path.

  1. def OAI.InvariantIsing.cavityFiniteCanonicalReplicaCovariance line 14
  2. lemma OAI.InvariantIsing.cavity_finite_replica_covariance_eq line 33
  3. theorem OAI.InvariantIsing.cavity_finite_replica_field_law line 53

    Source documentation

    The finite cavity root, actual independent forest, and replica-specific ordinary residuals have the canonical spectral Gaussian block law.

    theorem cavity_finite_replica_field_law (T : LabeledTree n) (σ : Fin r → LabeledLeaf n) :
    (((multivariateGaussian (0 : EuclideanSpace ℝ (Fin d))
      (cavityFiniteRootCovariance rho lam hrho hsum g p q)).prod
      (Measure.infinitePi (fun v : ForestVertex n => multivariateGaussian
        (0 : EuclideanSpace ℝ (Fin d))
        (cavityFiniteNoiseCovariance rho lam hrho hsum g p cut q (forestVertexDepth n v))))).prod
          (Measure.pi (fun _ : Fin r => multivariateGaussian
            (0 : EuclideanSpace ℝ (Fin d))
            (cavityFiniteCovariancePath rho lam hrho hsum g p q n)))).map
      (fun z => WithLp.toLp 2 (fun u : Fin r × Fin d =>
        (cavityLeafSum n z.1.1 (labeledNoiseLeaf _ n
          (T, markForestOfCoords _ n z.1.2) (σ u.1)) + z.2 u.1) u.2)) =
…

    Mentions: OAI.InvariantIsing.cavityFiniteRootCovariance, OAI.InvariantIsing.cavityFiniteNoiseCovariance, OAI.InvariantIsing.cavityFiniteCovariancePath, OAI.InvariantIsing.cavityLeafSum