OAI/Probability/Perceptron/Pressure/RootPartition.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SphericalPerceptronFreeEnergy.RootPartitionMatch line 12
  2. def OAI.SphericalPerceptronFreeEnergy.rootPartitionEncode line 16
  3. lemma OAI.SphericalPerceptronFreeEnergy.rootPartitionEncode_matches line 20
  4. def OAI.SphericalPerceptronFreeEnergy.rootPartitionEquiv line 26
  5. lemma OAI.SphericalPerceptronFreeEnergy.rootPartitionEquiv_apply line 54
  6. lemma OAI.SphericalPerceptronFreeEnergy.ennreal_tsum_fin_prod line 58
  7. lemma OAI.SphericalPerceptronFreeEnergy.ennreal_tsum_pi_prod line 69
  8. lemma OAI.SphericalPerceptronFreeEnergy.tsum_rootPartition line 77
  9. lemma OAI.SphericalPerceptronFreeEnergy.root_partition_sum_factor line 89
  10. lemma OAI.SphericalPerceptronFreeEnergy.tsum_pi_supported line 115
  11. lemma OAI.SphericalPerceptronFreeEnergy.indicator_forall_eq_prod line 137
  12. def OAI.SphericalPerceptronFreeEnergy.excludedBlockSum line 146
  13. def OAI.SphericalPerceptronFreeEnergy.DistinctAssignmentGood line 152
  14. lemma OAI.SphericalPerceptronFreeEnergy.distinctAssignmentGood_cons line 156
  15. lemma OAI.SphericalPerceptronFreeEnergy.excludedBlockSum_assignments line 170
  16. lemma OAI.SphericalPerceptronFreeEnergy.excludedBlockSum_embeddings line 197
  17. lemma OAI.SphericalPerceptronFreeEnergy.tsum_embedding_cast line 221
  18. lemma OAI.SphericalPerceptronFreeEnergy.tsum_embeddings_list_map line 228