OAI/Probability/SphericalField/Positivity/Patterns.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SphericalPerceptron.patternMatrices line 12
  2. lemma OAI.SphericalPerceptron.patternMatrices_measurable line 16
  3. def OAI.SphericalPerceptron.appendLabel line 28
  4. lemma OAI.SphericalPerceptron.appendLabel_last line 31
  5. lemma OAI.SphericalPerceptron.appendLabel_castSucc line 34
  6. lemma OAI.SphericalPerceptron.pattern_append_of_duplicate line 37
  7. theorem OAI.SphericalPerceptron.gg_pattern_append line 62
  8. lemma OAI.SphericalPerceptron.gg_pattern_append_nat line 79
  9. def OAI.SphericalPerceptron.tripleLabels line 92
  10. lemma OAI.SphericalPerceptron.appendLabel_tripleLabels line 94
  11. theorem OAI.SphericalPerceptron.gg_triple_pattern line 103