OAI/Probability/Perceptron/Variational/ContactFatou.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptronFreeEnergy.nonnegative_limit_integral_bound line 12
2. lemma OAI.SphericalPerceptronFreeEnergy.taylor_two_explicit line 40
3. lemma OAI.SphericalPerceptronFreeEnergy.second_symmetric_quotient_tendsto line 47
4. lemma OAI.SphericalPerceptronFreeEnergy.convex_symmetric_quotient_nonneg line 74
5. lemma OAI.SphericalPerceptronFreeEnergy.quadratic_contact_curvature_bound line 83
6. lemma OAI.SphericalPerceptronFreeEnergy.coupling_weighted_power_integrable line 118
7. lemma OAI.SphericalPerceptronFreeEnergy.coupling_tilt_memLp_two line 131
8. lemma OAI.SphericalPerceptronFreeEnergy.coupling_thermal_abs_sq_le line 145
9. lemma OAI.SphericalPerceptronFreeEnergy.coupling_tilt_center_triangle line 161