OAI/Probability/Perceptron/Variational/BlockFocus.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SphericalPerceptronFreeEnergy.indexedBlockSample line 11
2. def OAI.SphericalPerceptronFreeEnergy.indexedBlockFocused line 16
3. lemma OAI.SphericalPerceptronFreeEnergy.reindexed_shape_matches line 23
4. lemma OAI.SphericalPerceptronFreeEnergy.indexedBlockSample_shape line 40
5. lemma OAI.SphericalPerceptronFreeEnergy.indexedBlockFocused_shape line 55
6. lemma OAI.SphericalPerceptronFreeEnergy.indexedBlockSample_measurable line 71
7. lemma OAI.SphericalPerceptronFreeEnergy.indexedBlockFocused_measurable line 79
8. lemma OAI.SphericalPerceptronFreeEnergy.indexedBlockSample_eq_measure line 89
9. lemma OAI.SphericalPerceptronFreeEnergy.indexedBlockFocused_eq_measure line 101
10. theorem OAI.SphericalPerceptronFreeEnergy.indexedBlockFocused_integral line 119