OAI/Probability/Perceptron/Pressure/PatternMatrices.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptronFreeEnergy.block_event_swap line 11
  2. theorem OAI.SphericalPerceptronFreeEnergy.gg_duplicate_index line 26
  3. def OAI.SphericalPerceptronFreeEnergy.patternMatrices line 100
  4. lemma OAI.SphericalPerceptronFreeEnergy.patternMatrices_measurable line 104
  5. def OAI.SphericalPerceptronFreeEnergy.appendLabel line 116
  6. lemma OAI.SphericalPerceptronFreeEnergy.appendLabel_last line 119
  7. lemma OAI.SphericalPerceptronFreeEnergy.appendLabel_castSucc line 122
  8. lemma OAI.SphericalPerceptronFreeEnergy.pattern_append_of_duplicate line 125
  9. theorem OAI.SphericalPerceptronFreeEnergy.gg_pattern_append line 150
  10. lemma OAI.SphericalPerceptronFreeEnergy.gg_pattern_append_nat line 167
  11. def OAI.SphericalPerceptronFreeEnergy.tripleLabels line 180
  12. lemma OAI.SphericalPerceptronFreeEnergy.appendLabel_tripleLabels line 182
  13. theorem OAI.SphericalPerceptronFreeEnergy.gg_triple_pattern line 191
  14. def OAI.SphericalPerceptronFreeEnergy.replicaMean line 211
  15. lemma OAI.SphericalPerceptronFreeEnergy.inner_replicaMean line 213
  16. lemma OAI.SphericalPerceptronFreeEnergy.replicaMean_norm_sq_le line 221
  17. lemma OAI.SphericalPerceptronFreeEnergy.inner_replicaMean_eq line 249
  18. lemma OAI.SphericalPerceptronFreeEnergy.duplicate_blocks_bound line 258
  19. lemma OAI.SphericalPerceptronFreeEnergy.arbitrary_duplicate_blocks_equal line 298
  20. lemma OAI.SphericalPerceptronFreeEnergy.replicaMean_norm_le_one line 315
  21. lemma OAI.SphericalPerceptronFreeEnergy.inner_replicaMean_le line 330
  22. lemma OAI.SphericalPerceptronFreeEnergy.le_inner_replicaMean line 342
  23. lemma OAI.SphericalPerceptronFreeEnergy.duplicate_ordered_blocks_bound line 354
  24. lemma OAI.SphericalPerceptronFreeEnergy.posSemidef_standard_basis_inner line 389
  25. def OAI.SphericalPerceptronFreeEnergy.triangleConstraints line 397
  26. lemma OAI.SphericalPerceptronFreeEnergy.triangleConstraints_measurable line 403