OAI/Probability/SphericalField/Positivity/Cliques.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SphericalPerceptron.OverlapBlock line 15
  2. def OAI.SphericalPerceptron.overlapBlock line 17
  3. def OAI.SphericalPerceptron.GhirlandaGuerra line 20
  4. def OAI.SphericalPerceptron.negativeMatrices line 28
  5. def OAI.SphericalPerceptron.negativeClique line 31
  6. lemma OAI.SphericalPerceptron.negativeMatrices_measurable line 34
  7. lemma OAI.SphericalPerceptron.overlapBlock_measurable line 46
  8. lemma OAI.SphericalPerceptron.negativeClique_measurable line 55
  9. lemma OAI.SphericalPerceptron.mem_negativeClique line 61
  10. lemma OAI.SphericalPerceptron.negativeClique_succ line 65
  11. lemma OAI.SphericalPerceptron.negativeClique_two line 85
  12. lemma OAI.SphericalPerceptron.measureReal_inter_iInter_lower line 97
  13. lemma OAI.SphericalPerceptron.gg_negativeClique_extension line 111
  14. lemma OAI.SphericalPerceptron.negative_gram_sum_bound line 171