OAI/Probability/Perceptron/Interpolation/IntegrableReplicaGibbs.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptronFreeEnergy.tilt_mean_twice_of_integrable line 13
2. lemma OAI.SphericalPerceptronFreeEnergy.tiltMean_bound_general line 28
3. lemma OAI.SphericalPerceptronFreeEnergy.replica_exp_integrable line 36
4. lemma OAI.SphericalPerceptronFreeEnergy.tilt_law_apply_of_integrable line 44
5. lemma OAI.SphericalPerceptronFreeEnergy.tilt_law_pi_of_integrable line 52
6. lemma OAI.SphericalPerceptronFreeEnergy.gibbsReplicaMean_integral_of_integrable line 72
7. lemma OAI.SphericalPerceptronFreeEnergy.gibbsReplicaMean_bound_of_integrable line 80
8. lemma OAI.SphericalPerceptronFreeEnergy.gibbsReplicaMean_coordinate_of_integrable line 87
9. lemma OAI.SphericalPerceptronFreeEnergy.gibbsReplicaMean_sum_of_integrable line 98
10. lemma OAI.SphericalPerceptronFreeEnergy.gibbsReplicaMean_potential_of_integrable line 111
11. lemma OAI.SphericalPerceptronFreeEnergy.gibbsReplicaMean_product_of_integrable line 121