OAI/Probability/InvariantIsing/Gaussian/MPClippedTransform.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The literal MP law is fixed by clipping to its nonnegative support interval.

  1. lemma OAI.InvariantIsing.marchenkoPastur_mem_nonnegative_interval line 10
  2. lemma OAI.InvariantIsing.marchenkoPastur_clipped_transform line 17