OAI/Combinatorics/MatchingPSD/TableMoments.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MatchingSmoothing.weighted_common_fiber_bound line 14
  2. lemma OAI.MatchingSmoothing.weighted_table_kernel_bound line 36
  3. lemma OAI.MatchingSmoothing.weighted_table_kernel_moment line 52
  4. def OAI.MatchingSmoothing.threeEdgeType line 84
  5. def OAI.MatchingSmoothing.typeMultiplicity line 87
  6. lemma OAI.MatchingSmoothing.threeEdgeType_surjective line 89
  7. lemma OAI.MatchingSmoothing.card_threeEdgeType_fiber line 91
  8. lemma OAI.MatchingSmoothing.threeEdgeType_symm line 95
  9. lemma OAI.MatchingSmoothing.typeMultiplicity_pos line 98
  10. lemma OAI.MatchingSmoothing.endpoint_type_identity line 101
  11. def OAI.MatchingSmoothing.pairColorEquiv line 117
  12. def OAI.MatchingSmoothing.threeTable line 123
  13. def OAI.MatchingSmoothing.tableGamma line 126
  14. def OAI.MatchingSmoothing.tablePi line 130
  15. lemma OAI.MatchingSmoothing.histogram_cast_sum line 134
  16. lemma OAI.MatchingSmoothing.tableGamma_hermitian line 143
  17. lemma OAI.MatchingSmoothing.tableGamma_nonneg line 149
  18. lemma OAI.MatchingSmoothing.tableGamma_rowsum line 155
  19. lemma OAI.MatchingSmoothing.tablePi_pos line 173
  20. lemma OAI.MatchingSmoothing.tablePi_sum line 179
  21. lemma OAI.MatchingSmoothing.pairWeight_tableGamma_eq line 186
  22. lemma OAI.MatchingSmoothing.pairWeight_tableGamma_constant line 193
  23. lemma OAI.MatchingSmoothing.tableGamma_integer_mean_lower line 198
  24. lemma OAI.MatchingSmoothing.threeTable_histogram_eq line 230
  25. lemma OAI.MatchingSmoothing.histogram_product_mass_le_one line 249
  26. lemma OAI.MatchingSmoothing.vertexSqrtWeight_sq line 277
  27. lemma OAI.MatchingSmoothing.pairWeight_normalized line 288
  28. lemma OAI.MatchingSmoothing.three_table_kernel_moment line 301