OAI/Computability/VertexCover/Analysis/BatchFunctionOwnLipschitz.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.VertexCover.Cube.integrable_continuous line 44
2. theorem OAI.VertexCover.Cube.integrable_continuous_block line 50
3. def OAI.VertexCover.LabelCover.batchLaw line 62
4. instance OAI.VertexCover.LabelCover.batchLaw_probability line 65
5. theorem OAI.VertexCover.LabelCover.canonicalGradient_ae_cube line 70
6. theorem OAI.VertexCover.LabelCover.batchFunction_integrable line 82
7. theorem OAI.VertexCover.LabelCover.batchSum_update_sub line 88
8. theorem OAI.VertexCover.LabelCover.batchFunction_own_lipschitz line 101