OAI/Probability/SphericalField/Positivity/Arrays.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SphericalPerceptron.OverlapArray line 12
  2. def OAI.SphericalPerceptron.relabelArray line 13
  3. def OAI.SphericalPerceptron.OverlapSwapInvariant line 16
  4. def OAI.SphericalPerceptron.copyIndex line 19
  5. def OAI.SphericalPerceptron.copyBlock line 21
  6. def OAI.SphericalPerceptron.copyEvent line 24
  7. lemma OAI.SphericalPerceptron.copyIndex_self line 27
  8. lemma OAI.SphericalPerceptron.copyBlock_measurable line 33
  9. lemma OAI.SphericalPerceptron.copyEvent_measurable line 37
  10. lemma OAI.SphericalPerceptron.copyBlock_self line 41
  11. lemma OAI.SphericalPerceptron.copyIndex_relabel line 46
  12. lemma OAI.SphericalPerceptron.copyBlock_relabel line 54
  13. lemma OAI.SphericalPerceptron.copyEvent_relabel line 60
  14. def OAI.SphericalPerceptron.uniqueEvent line 66
  15. lemma OAI.SphericalPerceptron.uniqueEvent_measurable line 69
  16. lemma OAI.SphericalPerceptron.uniqueEvent_disjoint line 76
  17. lemma OAI.SphericalPerceptron.uniqueEvent_probability_bound line 83
  18. lemma OAI.SphericalPerceptron.uniqueEvent_preimage line 94
  19. lemma OAI.SphericalPerceptron.uniqueCopy_probability_bound line 112
  20. def OAI.SphericalPerceptron.prefixBlock line 140
  21. lemma OAI.SphericalPerceptron.prefixBlock_measurable line 143
  22. def OAI.SphericalPerceptron.starMatrices line 147
  23. def OAI.SphericalPerceptron.starEvent line 152
  24. lemma OAI.SphericalPerceptron.starMatrices_measurable line 156
  25. lemma OAI.SphericalPerceptron.starEvent_measurable line 166
  26. lemma OAI.SphericalPerceptron.starEvent_preimage line 178
  27. lemma OAI.SphericalPerceptron.starEvent_succ line 193
  28. lemma OAI.SphericalPerceptron.starEvent_zero line 209
  29. lemma OAI.SphericalPerceptron.gg_star_recurrence line 218