CavityResidualReplica.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Countably many cavity replicas with one independent terminal Gaussian residual per replica. The residual family is independent of the whole innovation cascade, including coincidences of sampled leaves.

lemma OAI.InvariantIsing.cavity_measurable_prod_const line 15
lemma OAI.InvariantIsing.cavity_infinitePi_zip line 28
lemma OAI.InvariantIsing.cavity_replica_product_mixture line 56

theorem OAI.InvariantIsing.cavity_quadratic_residual_replica_law line 87

Source documentation

The whole transformed replica sequence is sampled from the independent innovation tree, together with an independent iid family of ordinary terminal Gaussian residuals.

theorem cavity_quadratic_residual_replica_law {d : ℕ} (n : ℕ)
    (K : Matrix (Fin d) (Fin d) ℝ)
    (H S : ℕ → Matrix (Fin d) (Fin d) ℝ) (b : ℕ → ℝ)
    (hbCascade : CascadeExponents n b)
    (hK : K.transpose = K) (hH : ∀ i, (H i).transpose = H i)
    (hS : ∀ i, (S i).PosSemidef) (hb : ∀ i, 0 < b i)
    (hdet : ∀ i, IsUnit (1 - H i * K).det)
    (hΔ : ∀ i, H i - H (i + 1) = b i • S i)
    (hQ : ∀ i, (cavityFactorPrecision
      (b i • cavityBackwardQuadratic K (H (i + 1))) (CFC.sqrt (S i))).PosDef)
    (hR : (H n).PosSemidef)
    (hQR : (cavityFactorPrecision K (CFC.sqrt (H n))).PosDef)
…

Mentions: OAI.InvariantIsing.cavityFactorPrecision, OAI.InvariantIsing.cavityBackwardQuadratic

theorem OAI.InvariantIsing.cavity_residual_replica_path_law line 153

Source documentation

The independent residual sequence remains independent after the sampled innovation leaves are represented by their common-prefix paths.

theorem cavity_residual_replica_path_law {d : ℕ} (n : ℕ) (b : ℕ → ℝ)
    (hb : CascadeExponents n b) (μ : ℕ → ProbabilityMeasure (EuclideanSpace ℝ (Fin d)))
    (κ : Measure (EuclideanSpace ℝ (Fin d))) [IsProbabilityMeasure κ] :
    (((markedReplicaLaw n b μ).prod (Measure.infinitePi (fun _ : ℕ => κ))).map
      (fun p => fun i => (p.1 i, p.2 i))).map
        (fun σ => (replicaMarkPath n (fun i => (σ i).1), fun i => (σ i).2)) =
      (((cascadeReplicaLaw n b).prod (Measure.infinitePi
        (fun v : ForestVertex n => (μ (forestVertexDepth n v) : Measure _)))).prod
          (Measure.infinitePi (fun _ : ℕ => κ))).map
            (fun p => (coordinateMarkPath n p.1, p.2)) := by
…