CavityProjectedInnovation.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The Schur field identity identifies the covariance of each projected quadratic innovation with a scalar increment. This is the finite matrix step in the identification of the cavity field path.

theorem OAI.InvariantIsing.cavity_projected_resolvent_difference line 16

theorem OAI.InvariantIsing.cavity_projected_innovation_covariance line 32

Source documentation

The independent innovation covariance from cav:q-innovations, after projection to the cavity sites, is a scalar resolvent difference.

theorem cavity_projected_innovation_covariance {d n : ℕ}
    (K P C S : Matrix (Fin d) (Fin d) ℝ) (L : Matrix (Fin d) (Fin n) ℝ)
    (C₀ : Matrix (Fin n) (Fin n) ℝ) (rP rC ζ : ℝ) (hζ : ζ ≠ 0)
    (hK : K.transpose = K) (hCsym : C.transpose = C)
    (hPdet : IsUnit (1 - P * K).det) (hCdet : IsUnit (1 - C * K).det)
    (hΔ : P - C = ζ • S)
    (hP : C₀ + L.transpose * cavityResolvent K P * L = rP • 1)
    (hC : C₀ + L.transpose * cavityResolvent K C * L = rC • 1) :
    L.transpose * ((1 - P * K)⁻¹ * S * ((1 - C * K)⁻¹).transpose) * L =
      ((rP - rC) / ζ) • 1 := by
…

Mentions: OAI.InvariantIsing.cavityResolvent

theorem OAI.InvariantIsing.cavity_projected_innovation_law line 53

Source documentation

The exact projected Gaussian law at one independent innovation. Its scalar variance is specified by the two Schur field values.

theorem cavity_projected_innovation_law {d n : ℕ}
    (K P C S : Matrix (Fin d) (Fin d) ℝ) (L : Matrix (Fin d) (Fin n) ℝ)
    (C₀ : Matrix (Fin n) (Fin n) ℝ) (rP rC ζ : ℝ) (hζ : ζ ≠ 0)
    (hK : K.transpose = K) (hCsym : C.transpose = C)
    (hPdet : IsUnit (1 - P * K).det) (hCdet : IsUnit (1 - C * K).det)
    (hΔ : P - C = ζ • S)
    (hP : C₀ + L.transpose * cavityResolvent K P * L = rP • 1)
    (hC : C₀ + L.transpose * cavityResolvent K C * L = rC • 1)
    (hcov : ((1 - P * K)⁻¹ * S * ((1 - C * K)⁻¹).transpose).PosSemidef)
    (v : ℝ≥0) (hv : (v : ℝ) = (rP - rC) / ζ) :
    MeasurePreserving (fun z : EuclideanSpace ℝ (Fin d) =>
      WithLp.ofLp (L.transpose.toEuclideanLin z))
…

Mentions: OAI.InvariantIsing.cavityResolvent