OAI/Probability/Perceptron/Interpolation/CountableGaussianReplicaIBP.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptronFreeEnergy.countableGaussian_replica_coordinate_ibp line 14
2. lemma OAI.SphericalPerceptronFreeEnergy.gaussianHamiltonian_replica_coordinate_ibp line 57
3. lemma OAI.SphericalPerceptronFreeEnergy.integrable_tiltLaw_of_weighted line 78
4. lemma OAI.SphericalPerceptronFreeEnergy.replicaMean_varying_measurable line 89
5. lemma OAI.SphericalPerceptronFreeEnergy.replicaMean_energy_bound line 106
6. lemma OAI.SphericalPerceptronFreeEnergy.replicaMean_energy_sub line 141