OAI/Probability/InvariantIsing/Core/PositiveRationalApproximation.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Positive rational approximations to a finite probability vector, with explicit integer multiplicities.

  1. def OAI.InvariantIsing.positiveApproxCount line 15
  2. lemma OAI.InvariantIsing.positiveApproxCount_pos line 17
  3. lemma OAI.InvariantIsing.positiveApproxCount_ratio line 21
  4. def OAI.InvariantIsing.positiveApproxDenominator line 42
  5. lemma OAI.InvariantIsing.positiveApproxDenominator_pos line 45
  6. lemma OAI.InvariantIsing.positiveApproxWeights_tendsto line 51
  7. def OAI.InvariantIsing.positiveApproxWeights line 66
  8. lemma OAI.InvariantIsing.positiveApproxWeights_pos line 69
  9. lemma OAI.InvariantIsing.positiveApproxWeights_sum line 74