OAI/Probability/Perceptron/Interpolation/OverlapBlock.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SphericalPerceptronFreeEnergy.OverlapBlock line 16
  2. def OAI.SphericalPerceptronFreeEnergy.overlapBlock line 18
  3. def OAI.SphericalPerceptronFreeEnergy.GhirlandaGuerra line 21
  4. def OAI.SphericalPerceptronFreeEnergy.negativeMatrices line 29
  5. def OAI.SphericalPerceptronFreeEnergy.negativeClique line 32
  6. lemma OAI.SphericalPerceptronFreeEnergy.negativeMatrices_measurable line 35
  7. lemma OAI.SphericalPerceptronFreeEnergy.overlapBlock_measurable line 47
  8. lemma OAI.SphericalPerceptronFreeEnergy.negativeClique_measurable line 56
  9. lemma OAI.SphericalPerceptronFreeEnergy.mem_negativeClique line 62
  10. lemma OAI.SphericalPerceptronFreeEnergy.negativeClique_succ line 66
  11. lemma OAI.SphericalPerceptronFreeEnergy.negativeClique_two line 86
  12. lemma OAI.SphericalPerceptronFreeEnergy.measureReal_inter_iInter_lower line 98
  13. lemma OAI.SphericalPerceptronFreeEnergy.gg_negativeClique_extension line 112
  14. lemma OAI.SphericalPerceptronFreeEnergy.negative_gram_sum_bound line 172
  15. lemma OAI.SphericalPerceptronFreeEnergy.negativeClique_null line 197
  16. theorem OAI.SphericalPerceptronFreeEnergy.gg_negative_threshold_null line 216
  17. theorem OAI.SphericalPerceptronFreeEnergy.gg_overlap_nonnegative line 242
  18. lemma OAI.SphericalPerceptronFreeEnergy.gg_star_growth_impossible line 260