OAI/Probability/Perceptron/Cavity/CavityFreshReplacement.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptronFreeEnergy.cavityNormMoment_two line 11
  2. lemma OAI.SphericalPerceptronFreeEnergy.cavityNormMoment_one_le line 23
  3. def OAI.SphericalPerceptronFreeEnergy.cavityFreshMajorant line 34
  4. lemma OAI.SphericalPerceptronFreeEnergy.cavity_fresh_pattern_error line 39
  5. lemma OAI.SphericalPerceptronFreeEnergy.cavity_fresh_pattern_sum_error line 77
  6. lemma OAI.SphericalPerceptronFreeEnergy.cavity_fresh_log_replacement line 89
  7. lemma OAI.SphericalPerceptronFreeEnergy.cavity_row_norm_integrable line 112
  8. lemma OAI.SphericalPerceptronFreeEnergy.cavity_row_norm_mean line 119
  9. lemma OAI.SphericalPerceptronFreeEnergy.cavityFreshMajorant_integrable line 130
  10. lemma OAI.SphericalPerceptronFreeEnergy.cavityFreshMajorant_mean line 138
  11. lemma OAI.SphericalPerceptronFreeEnergy.cavityFreshMajorant_mean_bound line 154
  12. lemma OAI.SphericalPerceptronFreeEnergy.cavityFreshMajorant_mean_tendsto line 181