OAI/Combinatorics/MatchingPSD/IncidenceKernels.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MatchingSmoothing.sum_smul_eq line 14
  2. lemma OAI.MatchingSmoothing.sum_group_smul_eq line 18
  3. lemma OAI.MatchingSmoothing.group_smul_sum_card line 24
  4. lemma OAI.MatchingSmoothing.invariant_kernel_sum line 36
  5. lemma OAI.MatchingSmoothing.invariant_kernel_double_sum_group line 45
  6. lemma OAI.MatchingSmoothing.trace_normalized_kernel_sq line 61
  7. lemma OAI.MatchingSmoothing.trace_normalized_invariant_kernel_sq line 74
  8. def OAI.MatchingSmoothing.incidence line 95
  9. def OAI.MatchingSmoothing.commonIncidence line 98
  10. lemma OAI.MatchingSmoothing.commonIncidence_eq line 102
  11. lemma OAI.MatchingSmoothing.commonIncidence_symm line 111
  12. def OAI.MatchingSmoothing.incidenceKernel line 115
  13. def OAI.MatchingSmoothing.incidenceOperator line 118
  14. lemma OAI.MatchingSmoothing.incidenceKernel_symm line 122
  15. lemma OAI.MatchingSmoothing.incidenceOperator_eq line 128
  16. lemma OAI.MatchingSmoothing.incidenceOperator_posSemidef line 138
  17. def OAI.MatchingSmoothing.conditionalAverage line 146
  18. lemma OAI.MatchingSmoothing.conditionalAverage_energy line 150