OAI/Probability/Perceptron/Pressure/IndexedTerminalProduct.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptronFreeEnergy.cascadeTiltedStep_parallel line 16
2. lemma OAI.SphericalPerceptronFreeEnergy.cascadeTiltedStep_markov line 39
3. lemma OAI.SphericalPerceptronFreeEnergy.pathCorrelation_one line 48
4. lemma OAI.SphericalPerceptronFreeEnergy.indexed_terminal_product_pair_integral line 53
5. def OAI.SphericalPerceptronFreeEnergy.indexedTerminalBaseKernel line 95
6. instance OAI.SphericalPerceptronFreeEnergy.(instance at line 98) line 98
7. def OAI.SphericalPerceptronFreeEnergy.indexedTerminalEnergy line 102
8. lemma OAI.SphericalPerceptronFreeEnergy.indexedTerminalEnergy_measurable line 106
9. def OAI.SphericalPerceptronFreeEnergy.indexedTerminalPairMean line 112
10. lemma OAI.SphericalPerceptronFreeEnergy.indexedTerminalPairMean_measurable line 120
11. lemma OAI.SphericalPerceptronFreeEnergy.indexedTerminalPairMean_eq line 145
12. lemma OAI.SphericalPerceptronFreeEnergy.indexedTerminalPairMean_integral line 165
13. lemma OAI.SphericalPerceptronFreeEnergy.indexedTerminalPairMean_bound line 180
14. lemma OAI.SphericalPerceptronFreeEnergy.indexedTerminalPairMean_independent_arrays line 203