OAI/Probability/Perceptron/Cavity/BulkReplicaStein.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SphericalPerceptronFreeEnergy.bulkMoment line 12
  2. lemma OAI.SphericalPerceptronFreeEnergy.bulkReplicaMean_integrable line 15
  3. lemma OAI.SphericalPerceptronFreeEnergy.bulkReplicaY_measurable line 23
  4. lemma OAI.SphericalPerceptronFreeEnergy.bulkReplicaY_bound line 35
  5. lemma OAI.SphericalPerceptronFreeEnergy.bulkReplicaY_integrable line 49
  6. lemma OAI.SphericalPerceptronFreeEnergy.bulkPowerPair_measurable line 61
  7. lemma OAI.SphericalPerceptronFreeEnergy.bulkPowerPair_bound line 65
  8. lemma OAI.SphericalPerceptronFreeEnergy.bulkReplicaSum_bound line 70
  9. lemma OAI.SphericalPerceptronFreeEnergy.bulk_fixed_replica_ibp line 80
  10. lemma OAI.SphericalPerceptronFreeEnergy.bulk_rate_identity line 136
  11. lemma OAI.SphericalPerceptronFreeEnergy.bulkScale_sq_le line 152
  12. def OAI.SphericalPerceptronFreeEnergy.bulkNormalizedDeviation line 160
  13. lemma OAI.SphericalPerceptronFreeEnergy.bulkNormalizedDeviation_nonneg line 163
  14. lemma OAI.SphericalPerceptronFreeEnergy.bulkNormalizedDeviation_measurable line 169
  15. lemma OAI.SphericalPerceptronFreeEnergy.bulkNormalizedDeviation_integrable line 172
  16. def OAI.SphericalPerceptronFreeEnergy.bulkDeviationRate line 175
  17. lemma OAI.SphericalPerceptronFreeEnergy.bulkNormalizedDeviation_integral_bound line 179
  18. lemma OAI.SphericalPerceptronFreeEnergy.bulkDeviationRate_tendsto line 208