OAI/Combinatorics/MatchingPSD/PermutationSmoothing.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MatchingSmoothing.predicateAverage_equiv line 13
  2. lemma OAI.MatchingSmoothing.predicateAverage_eq_expect line 23
  3. def OAI.MatchingSmoothing.lowProjection line 32
  4. lemma OAI.MatchingSmoothing.lowProjection_mem line 36
  5. lemma OAI.MatchingSmoothing.lowProjection_equivariant line 40
  6. lemma OAI.MatchingSmoothing.predicateAverage_relabel line 48
  7. lemma OAI.MatchingSmoothing.expect_perm_colorings line 59
  8. def OAI.MatchingSmoothing.tableEnergy line 69
  9. lemma OAI.MatchingSmoothing.fiberAverage_eq_predicateAverage line 73
  10. lemma OAI.MatchingSmoothing.fiberEnergy_eq line 79
  11. lemma OAI.MatchingSmoothing.permutation_energy_eq line 88
  12. lemma OAI.MatchingSmoothing.uniform_permutation_smoothing line 102