OAI/Probability/SphericalField/Positivity/Triangles.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SphericalPerceptron.triangleEvent line 16
  2. lemma OAI.SphericalPerceptron.triangleEvent_pattern line 19
  3. lemma OAI.SphericalPerceptron.gg_triangleEvent_null line 30
  4. lemma OAI.SphericalPerceptron.exists_rational_triangle_box line 48
  5. lemma OAI.SphericalPerceptron.gg_no_ordered_crossing line 61
  6. lemma OAI.SphericalPerceptron.gram_array_symmetric line 92
  7. theorem OAI.SphericalPerceptron.gg_ultrametric line 101
  8. abbrev OAI.SphericalPerceptron.PairedOverlapArray line 127
  9. abbrev OAI.SphericalPerceptron.PairedOverlapBlock line 128
  10. def OAI.SphericalPerceptron.pairedBlock line 130
  11. def OAI.SphericalPerceptron.pairedRelabel line 133
  12. def OAI.SphericalPerceptron.PairedSwapInvariant line 136
  13. def OAI.SphericalPerceptron.JointGhirlandaGuerra line 139
  14. def OAI.SphericalPerceptron.scalarArray line 147
  15. def OAI.SphericalPerceptron.scalarBlock line 150
  16. lemma OAI.SphericalPerceptron.scalarArray_measurable line 153
  17. lemma OAI.SphericalPerceptron.scalarBlock_measurable line 158
  18. lemma OAI.SphericalPerceptron.scalarArray_swap_invariant line 163
  19. lemma OAI.SphericalPerceptron.scalarArray_gg line 177