OAI/Probability/InvariantIsing/Cavity/CavityProjectionLimit.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The Gram correction leaves the Gaussian projection limit unchanged. The Slutsky step allows arbitrary dependence between the raw projections and their normalizing Gram matrix.

  1. lemma OAI.InvariantIsing.cavityGaussian_correction_measurable line 17
  2. lemma OAI.InvariantIsing.cavityGaussian_correction_inMeasure line 22
  3. def OAI.InvariantIsing.cavityCorrectProjection line 32
  4. lemma OAI.InvariantIsing.cavityCorrectProjection_one line 37
  5. lemma OAI.InvariantIsing.continuous_cavityCorrectProjection line 42
  6. lemma OAI.InvariantIsing.cavityCorrectProjection_raw_apply line 48
  7. theorem OAI.InvariantIsing.cavityRawProjection_tendstoInDistribution line 61
  8. theorem OAI.InvariantIsing.cavityCorrectProjection_tendstoInDistribution line 81
  9. def OAI.InvariantIsing.cavityFrameProjection line 95
  10. theorem OAI.InvariantIsing.cavityFrameProjection_tendstoInDistribution line 102

    Source documentation

    The fixed number of normalized Gaussian directions has the same Gaussian replica-projection limit as the unnormalized directions.

    theorem cavityFrameProjection_tendstoInDistribution {r q : ℕ}
    (N : ℕ → ℕ) (hN : Tendsto N atTop atTop)
    (v : (k : ℕ) → Fin r → Fin (N k) → ℝ)
    (S : Matrix (Fin r × Fin q) (Fin r × Fin q) ℝ) (hS : S.PosSemidef)
    (hcov : Tendsto (fun k => cavityProjectionMatrix (q := q) (v k) *
…

    Mentions: OAI.InvariantIsing.cavityProjectionMatrix

  11. def OAI.InvariantIsing.cavityReplicaCovariance line 118
  12. lemma OAI.InvariantIsing.cavityProjection_covariance_tendsto line 122
  13. theorem OAI.InvariantIsing.cavityFrameProjection_tendsto_of_replicaGram line 141