OAI/Probability/Perceptron/Variational/VarianceProdMemLp.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptronFreeEnergy.variance_prod_le_memLp line 21
2. lemma OAI.SphericalPerceptronFreeEnergy.vectorLogPartition_bound line 51
3. lemma OAI.SphericalPerceptronFreeEnergy.vectorLogPartition_data_bound line 64
4. lemma OAI.SphericalPerceptronFreeEnergy.vectorLogPartition_mixed_variance line 79
5. lemma OAI.SphericalPerceptronFreeEnergy.integral_observable_factorization_bound line 150
6. lemma OAI.SphericalPerceptronFreeEnergy.replicaMean_energy_factorization_bound line 174
7. lemma OAI.SphericalPerceptronFreeEnergy.measurable_tiltMean_param line 193
8. lemma OAI.SphericalPerceptronFreeEnergy.measurable_replicaMean_param line 200
9. lemma OAI.SphericalPerceptronFreeEnergy.annealed_replica_energy_factorization_bound line 209