OAI/Probability/InvariantIsing/Cavity/CavityReplicaNodeProjection.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The finite set of Gaussian nodes visited by a tuple of cavity leaves. Each replica keeps the common root and shared edges, and receives its own ordinary terminal residual.

  1. lemma OAI.InvariantIsing.cavity_nodeAt_injective line 16
  2. def OAI.InvariantIsing.cavityReplicaNodePath line 23
  3. def OAI.InvariantIsing.cavityReplicaNodeSupport line 29
  4. def OAI.InvariantIsing.cavityReplicaNodeWeight line 34
  5. lemma OAI.InvariantIsing.cavityReplicaNodePath_subset line 39
  6. lemma OAI.InvariantIsing.cavity_replica_node_sum line 45
  7. theorem OAI.InvariantIsing.cavity_replica_node_field line 81

    Source documentation

    The node representation is pointwise the original root-plus-forest field, including the independent residual of each replica.

    theorem cavity_replica_node_field {r d : ℕ} (n : ℕ) (σ : Fin r → LabeledLeaf n)
    (T : LabeledTree n)
    (p : (EuclideanSpace ℝ (Fin d) × (ForestVertex n → EuclideanSpace ℝ (Fin d))) ×
      (Fin r → EuclideanSpace ℝ (Fin d))) :
    cavityGaussianNodeSum (cavityReplicaNodeWeight n σ)
      (fun a => cavityReplicaNodeJoin n r p a) =
      WithLp.toLp 2 (fun q : Fin r × Fin d =>
        (cavityLeafSum n p.1.1 (labeledNoiseLeaf _ n
          (T, markForestOfCoords _ n p.1.2) (σ q.1)) + p.2 q.1) q.2) := by
…

    Mentions: OAI.InvariantIsing.cavityGaussianNodeSum, OAI.InvariantIsing.cavityReplicaNodeWeight, OAI.InvariantIsing.cavityReplicaNodeJoin, OAI.InvariantIsing.cavityLeafSum

  8. def OAI.InvariantIsing.cavityReplicaGaussianCovariance line 98
  9. theorem OAI.InvariantIsing.cavity_replica_gaussian_field_law line 107

    Source documentation

    Joint law of the actual cavity fields for any fixed tuple of leaves. The same root is retained in every replica; ordinary residuals are independent.

    theorem cavity_replica_gaussian_field_law {r d : ℕ} (n : ℕ)
    (S₀ R : Matrix (Fin d) (Fin d) ℝ) (S : ℕ → Matrix (Fin d) (Fin d) ℝ)
    (hS₀ : S₀.PosSemidef) (hR : R.PosSemidef) (hS : ∀ i, (S i).PosSemidef)
    (T : LabeledTree n) (σ : Fin r → LabeledLeaf n) :
    (((multivariateGaussian (0 : EuclideanSpace ℝ (Fin d)) S₀).prod
      (Measure.infinitePi (fun v : ForestVertex n => multivariateGaussian
        (0 : EuclideanSpace ℝ (Fin d)) (S (forestVertexDepth n v))))).prod
          (Measure.pi (fun _ : Fin r => multivariateGaussian
            (0 : EuclideanSpace ℝ (Fin d)) R))).map
      (fun p => WithLp.toLp 2 (fun q : Fin r × Fin d =>
        (cavityLeafSum n p.1.1 (labeledNoiseLeaf _ n
          (T, markForestOfCoords _ n p.1.2) (σ q.1)) + p.2 q.1) q.2)) =
…

    Mentions: OAI.InvariantIsing.cavityLeafSum