OAI/Probability/Perceptron/Cavity/BulkRadialIdentity.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptronFreeEnergy.bulkReplicaMean_sub_bounded line 12
  2. def OAI.SphericalPerceptronFreeEnergy.bulkRadialRow line 25
  3. def OAI.SphericalPerceptronFreeEnergy.bulkSecondRow line 26
  4. def OAI.SphericalPerceptronFreeEnergy.bulkRadialPairRow line 27
  5. lemma OAI.SphericalPerceptronFreeEnergy.bulkFreshRow_measurable line 29
  6. lemma OAI.SphericalPerceptronFreeEnergy.bulkRadialRow_measurable line 34
  7. lemma OAI.SphericalPerceptronFreeEnergy.bulkSecondRow_measurable line 37
  8. lemma OAI.SphericalPerceptronFreeEnergy.bulkRadialPairRow_measurable line 40
  9. def OAI.SphericalPerceptronFreeEnergy.Jet3.radialMark line 44
  10. lemma OAI.SphericalPerceptronFreeEnergy.bulkRadialRow_bound line 47
  11. lemma OAI.SphericalPerceptronFreeEnergy.bulk_radial_difference line 51
  12. lemma OAI.SphericalPerceptronFreeEnergy.bulk_radial_sum_eq line 64
  13. lemma OAI.SphericalPerceptronFreeEnergy.bulk_radial_pair_sum_eq line 75
  14. lemma OAI.SphericalPerceptronFreeEnergy.bulk_radial_sum_identity line 86
  15. lemma OAI.SphericalPerceptronFreeEnergy.bulkReplicaMean_add_bounded line 105
  16. lemma OAI.SphericalPerceptronFreeEnergy.bulkReplicaMean_mean_square_le line 118
  17. lemma OAI.SphericalPerceptronFreeEnergy.bulkReplicaMean_L2_tendsto line 137