OAI/Probability/Perceptron/Interpolation/TiltReplicaCoordinate.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptronFreeEnergy.tilt_replica_coordinate line 16
2. lemma OAI.SphericalPerceptronFreeEnergy.tilt_mean_sum line 25
3. lemma OAI.SphericalPerceptronFreeEnergy.tilt_replica_sum line 35
4. lemma OAI.SphericalPerceptronFreeEnergy.tilt_replica_new_product line 49
5. lemma OAI.SphericalPerceptronFreeEnergy.gaussianField_replica line 75
6. lemma OAI.SphericalPerceptronFreeEnergy.replicaPotential_add_field line 83
7. lemma OAI.SphericalPerceptronFreeEnergy.gaussian_replica_coordinate_ibp line 98
8. lemma OAI.SphericalPerceptronFreeEnergy.gamma_lintegral_positive_scale line 146
9. lemma OAI.SphericalPerceptronFreeEnergy.integrable_rpow_neg_of_laplace line 168
10. lemma OAI.SphericalPerceptronFreeEnergy.stablePoissonTotal_negative_integrable line 214
11. lemma OAI.SphericalPerceptronFreeEnergy.tilt_log_partition_deriv line 225
12. lemma OAI.SphericalPerceptronFreeEnergy.tilt_variance_eq line 230
13. lemma OAI.SphericalPerceptronFreeEnergy.tilt_mean_potential_monotone line 242
14. lemma OAI.SphericalPerceptronFreeEnergy.tilt_log_partition_convex line 250
15. lemma OAI.SphericalPerceptronFreeEnergy.convex_contact_derivative_bound line 262
16. lemma OAI.SphericalPerceptronFreeEnergy.poissonRandomMeasureLaw_superposition line 287
17. lemma OAI.SphericalPerceptronFreeEnergy.poissonRandomMeasureLaw_of_finite line 309
18. lemma OAI.SphericalPerceptronFreeEnergy.aemeasurable_randomMeasure_lintegral_of_finite line 333
19. lemma OAI.SphericalPerceptronFreeEnergy.poissonRandomMeasureLaw_ae_restrict_finite line 356
20. lemma OAI.SphericalPerceptronFreeEnergy.poissonRandomMeasureLaw_ae_null line 366
21. lemma OAI.SphericalPerceptronFreeEnergy.stablePoissonTotal_rpow_integrable line 376
22. lemma OAI.SphericalPerceptronFreeEnergy.log_sq_le_two_rpow line 384
23. lemma OAI.SphericalPerceptronFreeEnergy.stablePoissonTotal_weighted_log_sq_integrable line 405