OAI/Probability/InvariantIsing/Cavity/CavityGroupProjection.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Joint projections in the independent spectral groups. The output index retains the group, replica, and fresh-axis coordinates, so the limiting Gaussian law records independence between different groups.

  1. def OAI.InvariantIsing.cavityGroupProjectionMatrix line 16
  2. def OAI.InvariantIsing.cavityGroupRawProjection line 22
  3. lemma OAI.InvariantIsing.cavityGroupRawProjection_apply line 28
  4. theorem OAI.InvariantIsing.cavityGroupRawProjection_hasLaw line 41
  5. lemma OAI.InvariantIsing.cavityGroupGaussian_correction_measurable line 53
  6. lemma OAI.InvariantIsing.cavityGroupGaussian_correction_inMeasure line 60
  7. def OAI.InvariantIsing.cavityGroupCorrectProjection line 76
  8. lemma OAI.InvariantIsing.cavityGroupCorrectProjection_one line 81
  9. lemma OAI.InvariantIsing.continuous_cavityGroupCorrectProjection line 87
  10. def OAI.InvariantIsing.cavityGroupFrameProjection line 93
  11. lemma OAI.InvariantIsing.cavityGroupCorrectProjection_raw line 99
  12. theorem OAI.InvariantIsing.cavityGroupRawProjection_tendstoInDistribution line 113
  13. theorem OAI.InvariantIsing.cavityGroupFrameProjection_tendstoInDistribution line 135

    Source documentation

    Joint normalization does not alter the multigroup Gaussian limit. No independence between projections and their Gram corrections is needed.

    theorem cavityGroupFrameProjection_tendstoInDistribution {m r q : ℕ}
    (N : ℕ → Fin m → ℕ) (hN : ∀ a, Tendsto (fun k => N k a) atTop atTop)
    (v : (k : ℕ) → (a : Fin m) → Fin r → Fin (N k a) → ℝ)
    (S : Matrix (Fin m × (Fin r × Fin q)) (Fin m × (Fin r × Fin q)) ℝ)
    (hS : S.PosSemidef)
    (hcov : Tendsto (fun k => cavityGroupProjectionMatrix (q := q) (v k) *
…

    Mentions: OAI.InvariantIsing.cavityGroupProjectionMatrix