OAI/Probability/Perceptron/Variational/HeightWord.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SphericalPerceptronFreeEnergy.extendedFieldExponents line 11
  2. def OAI.SphericalPerceptronFreeEnergy.finiteFieldCDFLeft line 14
  3. lemma OAI.SphericalPerceptronFreeEnergy.extendedFieldExponents_castSucc line 17
  4. lemma OAI.SphericalPerceptronFreeEnergy.extendedFieldExponents_last line 30
  5. lemma OAI.SphericalPerceptronFreeEnergy.extendedFieldExponents_nonneg line 34
  6. lemma OAI.SphericalPerceptronFreeEnergy.extendedFieldExponents_heightIndex line 40
  7. lemma OAI.SphericalPerceptronFreeEnergy.sphericalHeatValue_compress line 44
  8. lemma OAI.SphericalPerceptronFreeEnergy.sphericalHeatValue_drop_last_one line 61
  9. lemma OAI.SphericalPerceptronFreeEnergy.finiteSphericalFieldValue_height_word line 75
  10. def OAI.SphericalPerceptronFreeEnergy.heightIndicator line 107
  11. lemma OAI.SphericalPerceptronFreeEnergy.heightIndicator_antitone line 109
  12. lemma OAI.SphericalPerceptronFreeEnergy.heightIndicator_weighted_sum line 118
  13. lemma OAI.SphericalPerceptronFreeEnergy.heightIndicator_distance_sum line 130
  14. lemma OAI.SphericalPerceptronFreeEnergy.finiteFieldCDFLeft_coupling_sub line 145
  15. lemma OAI.SphericalPerceptronFreeEnergy.finiteFieldCDFLeft_coupling_abs line 155
  16. lemma OAI.SphericalPerceptronFreeEnergy.finiteFieldCDFLeft_partition_cost line 164
  17. lemma OAI.SphericalPerceptronFreeEnergy.exists_common_height_partition line 193