OAI/Probability/Perceptron/Interpolation/OverlapArray.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SphericalPerceptronFreeEnergy.OverlapArray line 11
  2. def OAI.SphericalPerceptronFreeEnergy.relabelArray line 12
  3. def OAI.SphericalPerceptronFreeEnergy.OverlapSwapInvariant line 15
  4. def OAI.SphericalPerceptronFreeEnergy.copyIndex line 18
  5. def OAI.SphericalPerceptronFreeEnergy.copyBlock line 20
  6. def OAI.SphericalPerceptronFreeEnergy.copyEvent line 23
  7. lemma OAI.SphericalPerceptronFreeEnergy.copyIndex_self line 26
  8. lemma OAI.SphericalPerceptronFreeEnergy.copyBlock_measurable line 32
  9. lemma OAI.SphericalPerceptronFreeEnergy.copyEvent_measurable line 36
  10. lemma OAI.SphericalPerceptronFreeEnergy.copyBlock_self line 40
  11. lemma OAI.SphericalPerceptronFreeEnergy.copyIndex_relabel line 45
  12. lemma OAI.SphericalPerceptronFreeEnergy.copyBlock_relabel line 53
  13. lemma OAI.SphericalPerceptronFreeEnergy.copyEvent_relabel line 59
  14. def OAI.SphericalPerceptronFreeEnergy.uniqueEvent line 65
  15. lemma OAI.SphericalPerceptronFreeEnergy.uniqueEvent_measurable line 68
  16. lemma OAI.SphericalPerceptronFreeEnergy.uniqueEvent_disjoint line 75
  17. lemma OAI.SphericalPerceptronFreeEnergy.uniqueEvent_probability_bound line 82
  18. lemma OAI.SphericalPerceptronFreeEnergy.uniqueEvent_preimage line 93
  19. lemma OAI.SphericalPerceptronFreeEnergy.uniqueCopy_probability_bound line 111
  20. def OAI.SphericalPerceptronFreeEnergy.prefixBlock line 139
  21. lemma OAI.SphericalPerceptronFreeEnergy.prefixBlock_measurable line 142
  22. def OAI.SphericalPerceptronFreeEnergy.starMatrices line 146
  23. def OAI.SphericalPerceptronFreeEnergy.starEvent line 151
  24. lemma OAI.SphericalPerceptronFreeEnergy.starMatrices_measurable line 155
  25. lemma OAI.SphericalPerceptronFreeEnergy.starEvent_measurable line 165
  26. lemma OAI.SphericalPerceptronFreeEnergy.starEvent_preimage line 177
  27. lemma OAI.SphericalPerceptronFreeEnergy.starEvent_succ line 192
  28. lemma OAI.SphericalPerceptronFreeEnergy.starEvent_zero line 208
  29. lemma OAI.SphericalPerceptronFreeEnergy.gg_star_recurrence line 217
  30. def OAI.SphericalPerceptronFreeEnergy.duplicateEvent line 253
  31. lemma OAI.SphericalPerceptronFreeEnergy.duplicateEvent_measurable line 257
  32. lemma OAI.SphericalPerceptronFreeEnergy.duplicateEvent_relabel line 262
  33. lemma OAI.SphericalPerceptronFreeEnergy.duplicateEvent_null_future line 270
  34. lemma OAI.SphericalPerceptronFreeEnergy.star_unique_bound_of_no_duplication line 287
  35. lemma OAI.SphericalPerceptronFreeEnergy.edge_probability_swap line 318
  36. theorem OAI.SphericalPerceptronFreeEnergy.gg_duplicate_last line 326
  37. def OAI.SphericalPerceptronFreeEnergy.relabelBlock line 355
  38. def OAI.SphericalPerceptronFreeEnergy.replaceIndex line 358
  39. def OAI.SphericalPerceptronFreeEnergy.replaceBlock line 361
  40. def OAI.SphericalPerceptronFreeEnergy.replaceEvent line 364
  41. lemma OAI.SphericalPerceptronFreeEnergy.relabelBlock_measurable line 367
  42. lemma OAI.SphericalPerceptronFreeEnergy.replaceBlock_measurable line 372
  43. lemma OAI.SphericalPerceptronFreeEnergy.fin_swap_val line 377
  44. lemma OAI.SphericalPerceptronFreeEnergy.relabelBlock_swap line 381
  45. lemma OAI.SphericalPerceptronFreeEnergy.relabelArray_swap_swap line 387
  46. lemma OAI.SphericalPerceptronFreeEnergy.relabelBlock_swap_swap line 392
  47. lemma OAI.SphericalPerceptronFreeEnergy.replaceBlock_last line 397
  48. lemma OAI.SphericalPerceptronFreeEnergy.replaceBlock_swap line 404