OAI/Combinatorics/SquareDifference/TensorPair.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SquareDifference.pairPush line 20
  2. def OAI.SquareDifference.pairSample line 25
  3. lemma OAI.SquareDifference.pair_indicator_pi line 30
  4. lemma OAI.SquareDifference.tensorLaw_pair_sampling line 47
  5. def OAI.SquareDifference.piProductEquiv line 74
  6. lemma OAI.SquareDifference.expect_pi_product line 80
  7. lemma OAI.SquareDifference.tensorLaw_pair_product_sampling line 87
  8. lemma OAI.SquareDifference.tupleGoodLaw_pair_product line 100
  9. lemma OAI.SquareDifference.tensorLaw_squarePair_sampling line 106
  10. lemma OAI.SquareDifference.tensorGood_pair line 120
  11. lemma OAI.SquareDifference.expect_restrict_compl line 136
  12. lemma OAI.SquareDifference.tensorGood_frozen_pair line 156