OAI/Probability/Perceptron/Variational/TripleIndex.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptronFreeEnergy.triangleConstraints_diag line 14
  2. lemma OAI.SphericalPerceptronFreeEnergy.triangleConstraints_cut line 17
  3. def OAI.SphericalPerceptronFreeEnergy.tripleIndex line 26
  4. lemma OAI.SphericalPerceptronFreeEnergy.tripleLabels_tripleIndex line 29
  5. lemma OAI.SphericalPerceptronFreeEnergy.tripleIndex_ne line 34
  6. lemma OAI.SphericalPerceptronFreeEnergy.tripleIndex_inj line 40
  7. lemma OAI.SphericalPerceptronFreeEnergy.triangle_pattern_psd_bound line 49
  8. theorem OAI.SphericalPerceptronFreeEnergy.gg_triangle_pattern_bound line 85
  9. def OAI.SphericalPerceptronFreeEnergy.triangleEvent line 115
  10. lemma OAI.SphericalPerceptronFreeEnergy.triangleEvent_pattern line 118
  11. lemma OAI.SphericalPerceptronFreeEnergy.gg_triangleEvent_null line 129
  12. lemma OAI.SphericalPerceptronFreeEnergy.exists_rational_triangle_box line 147
  13. lemma OAI.SphericalPerceptronFreeEnergy.gg_no_ordered_crossing line 160
  14. lemma OAI.SphericalPerceptronFreeEnergy.gram_array_symmetric line 191
  15. theorem OAI.SphericalPerceptronFreeEnergy.gg_ultrametric line 200
  16. abbrev OAI.SphericalPerceptronFreeEnergy.PairedOverlapArray line 226
  17. abbrev OAI.SphericalPerceptronFreeEnergy.PairedOverlapBlock line 227
  18. def OAI.SphericalPerceptronFreeEnergy.pairedBlock line 229
  19. def OAI.SphericalPerceptronFreeEnergy.pairedRelabel line 232
  20. def OAI.SphericalPerceptronFreeEnergy.PairedSwapInvariant line 235
  21. def OAI.SphericalPerceptronFreeEnergy.JointGhirlandaGuerra line 238
  22. def OAI.SphericalPerceptronFreeEnergy.scalarArray line 246
  23. def OAI.SphericalPerceptronFreeEnergy.scalarBlock line 249
  24. lemma OAI.SphericalPerceptronFreeEnergy.scalarArray_measurable line 252
  25. lemma OAI.SphericalPerceptronFreeEnergy.scalarBlock_measurable line 257
  26. lemma OAI.SphericalPerceptronFreeEnergy.scalarArray_swap_invariant line 262
  27. lemma OAI.SphericalPerceptronFreeEnergy.scalarArray_gg line 276
  28. lemma OAI.SphericalPerceptronFreeEnergy.measurableSet_gram_arrays line 299
  29. lemma OAI.SphericalPerceptronFreeEnergy.scalarArray_ultrametric line 318
  30. def OAI.SphericalPerceptronFreeEnergy.UltrametricTriangle line 338
  31. lemma OAI.SphericalPerceptronFreeEnergy.gg_ultrametric_triangle line 341
  32. lemma OAI.SphericalPerceptronFreeEnergy.scalarArray_ultrametric_triangle line 358
  33. lemma OAI.SphericalPerceptronFreeEnergy.ultrametric_triangle_small_eq line 378
  34. lemma OAI.SphericalPerceptronFreeEnergy.ultrametric_sum_no_crossing line 388
  35. theorem OAI.SphericalPerceptronFreeEnergy.joint_gg_no_crossing line 404