OAI/Probability/Perceptron/Cavity/BulkTangentError.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptronFreeEnergy.bulkCovarianceDerivative_bound line 13
  2. def OAI.SphericalPerceptronFreeEnergy.bulkTangentDirection line 47
  3. lemma OAI.SphericalPerceptronFreeEnergy.bulkTangentDirection_continuous line 52
  4. lemma OAI.SphericalPerceptronFreeEnergy.bulkTangentDirection_cross line 62
  5. lemma OAI.SphericalPerceptronFreeEnergy.bulkTangentDirection_cross_bound line 72
  6. lemma OAI.SphericalPerceptronFreeEnergy.bulk_tangent_perturbation_bound line 88
  7. def OAI.SphericalPerceptronFreeEnergy.bulkPatternLinear line 110
  8. lemma OAI.SphericalPerceptronFreeEnergy.bulkPatternLinear_apply line 113
  9. def OAI.SphericalPerceptronFreeEnergy.ambientBulkHamiltonian line 119
  10. lemma OAI.SphericalPerceptronFreeEnergy.ambientBulkHamiltonian_eq line 123
  11. lemma OAI.SphericalPerceptronFreeEnergy.ambientBulkHamiltonian_contDiff line 129
  12. lemma OAI.SphericalPerceptronFreeEnergy.ambientBulkHamiltonian_deriv line 135
  13. lemma OAI.SphericalPerceptronFreeEnergy.bulk_gibbs_replica_tangent line 151