OAI/Probability/Perceptron/Cavity/CavityPerturbationCovariance.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptronFreeEnergy.bulkCovariance_bound line 11
  2. lemma OAI.SphericalPerceptronFreeEnergy.bulkCovariance_scaled_hasDerivAt line 34
  3. lemma OAI.SphericalPerceptronFreeEnergy.bulkCovariance_scaled_lipschitz line 48
  4. lemma OAI.SphericalPerceptronFreeEnergy.bulkCovariance_dimension_tail line 59
  5. theorem OAI.SphericalPerceptronFreeEnergy.cavity_bulk_covariance_bound line 92
  6. lemma OAI.SphericalPerceptronFreeEnergy.bulkScale_sq_eq_rpow line 117
  7. lemma OAI.SphericalPerceptronFreeEnergy.bulkScale_sq_shift_bound line 122
  8. lemma OAI.SphericalPerceptronFreeEnergy.bulkScale_sq_div_shift_bound line 142
  9. def OAI.SphericalPerceptronFreeEnergy.cavityBulkCovarianceError line 164
  10. lemma OAI.SphericalPerceptronFreeEnergy.cavityBulkCovarianceError_nonneg line 169
  11. lemma OAI.SphericalPerceptronFreeEnergy.cavity_bulk_covariance_shell line 172
  12. lemma OAI.SphericalPerceptronFreeEnergy.cavityBulkCovarianceError_tendsto line 185