OAI/Probability/Perceptron/Cascade/CavityCappedRPC.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptronFreeEnergy.cavityDiagonalAverage_bounds line 12
2. lemma OAI.SphericalPerceptronFreeEnergy.cavityResidualCapped_bounds line 28
3. lemma OAI.SphericalPerceptronFreeEnergy.cavityResidualCapped_pos line 35
4. lemma OAI.SphericalPerceptronFreeEnergy.cavityResidualCapped_log_bound line 40
5. theorem OAI.SphericalPerceptronFreeEnergy.cavity_capped_indexed_log_recursion line 51