OAI/Probability/Perceptron/Cavity/BulkReplicaDominated.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptronFreeEnergy.replicaMean_param_integrable_dominated line 13
  2. lemma OAI.SphericalPerceptronFreeEnergy.bulkReplicaMean_sum_dominated line 25
  3. def OAI.SphericalPerceptronFreeEnergy.bulkPatternSize line 42
  4. lemma OAI.SphericalPerceptronFreeEnergy.bulkPatternSize_integrable line 44
  5. lemma OAI.SphericalPerceptronFreeEnergy.bulkPatternFields_bound line 55
  6. def OAI.SphericalPerceptronFreeEnergy.bulkTangentPattern line 63
  7. lemma OAI.SphericalPerceptronFreeEnergy.bulkTangentPattern_measurable line 68
  8. lemma OAI.SphericalPerceptronFreeEnergy.bulkTangentPattern_bound line 75
  9. lemma OAI.SphericalPerceptronFreeEnergy.bulkTangentPattern_integrable line 89
  10. def OAI.SphericalPerceptronFreeEnergy.freshTangent line 98
  11. def OAI.SphericalPerceptronFreeEnergy.freshTangentPair line 103
  12. def OAI.SphericalPerceptronFreeEnergy.freshTangentTriple line 108
  13. lemma OAI.SphericalPerceptronFreeEnergy.freshTangent_measurable line 113
  14. lemma OAI.SphericalPerceptronFreeEnergy.freshTangentPair_measurable line 119
  15. lemma OAI.SphericalPerceptronFreeEnergy.freshTangentTriple_measurable line 125
  16. lemma OAI.SphericalPerceptronFreeEnergy.normalizedSpin_inner_bound line 131
  17. lemma OAI.SphericalPerceptronFreeEnergy.freshTangent_bound line 136
  18. lemma OAI.SphericalPerceptronFreeEnergy.freshTangentPair_bound line 149
  19. lemma OAI.SphericalPerceptronFreeEnergy.freshTangentTriple_bound line 162
  20. lemma OAI.SphericalPerceptronFreeEnergy.bulkFreshReplicaMean_integrable line 176
  21. lemma OAI.SphericalPerceptronFreeEnergy.bulkReplicaMean_last_integral line 189
  22. lemma OAI.SphericalPerceptronFreeEnergy.fresh_tangent_ibp line 227
  23. lemma OAI.SphericalPerceptronFreeEnergy.bulk_tangent_last_ibp line 252
  24. lemma OAI.SphericalPerceptronFreeEnergy.bulkReplicaMean_row_eq_last line 288
  25. lemma OAI.SphericalPerceptronFreeEnergy.bulk_tangent_row_ibp line 299