OAI/Probability/InvariantIsing/Gaussian/GaussianPatternPublishedInputs.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Marchenko–Pastur and Davidson–Szarek estimates for Gaussian-pattern matrices. MP1967, Theorem1 and examples pp.459,461, gives the displayed law and empirical limit. DS2001, TheoremII.13, gives the edge-excess and uniform-integrability consequences for the Gaussian rectangular matrix.

  1. def OAI.InvariantIsing.gaussianPatternCount line 17

    Also declared: ComparatorChallenges/InvariantIsing.lean:234 (same declaration text).

  2. def OAI.InvariantIsing.marchenkoPasturA line 18

    Also declared: ComparatorChallenges/InvariantIsing.lean:236 (same declaration text).

  3. def OAI.InvariantIsing.marchenkoPasturB line 19

    Also declared: ComparatorChallenges/InvariantIsing.lean:238 (same declaration text).

  4. def OAI.InvariantIsing.marchenkoPasturLower line 20

    Also declared: ComparatorChallenges/InvariantIsing.lean:240 (same declaration text).

  5. def OAI.InvariantIsing.marchenkoPasturMeasure line 22

    Also declared: ComparatorChallenges/InvariantIsing.lean:242 (same declaration text).

  6. structure OAI.InvariantIsing.MarchenkoPasturInput line 29

    Source documentation

    The fixed-aspect-ratio Gaussian specialization of MP1967, Theorem1.

    structure MarchenkoPasturInput (α : ℝ) (_hα : 0 < α) : Prop where
…
  7. structure OAI.InvariantIsing.DavidsonSzarekInput line 47

    Source documentation

    The edge and integrable-tail consequences of DS2001, TheoremII.13. The rank-deficient case uses the exact zero eigenvalues of the Gram matrix.

    structure DavidsonSzarekInput (α : ℝ) (_hα : 0 < α) : Prop where
…