OAI/Probability/GaussianReplacement/Streaming.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CurrentProjection.StreamKernel.CompletedLearner.borel_estimateLaw_ae line 19
2. lemma OAI.CurrentProjection.StreamKernel.CompletedLearner.borel_uniformSuccess line 56
3. lemma OAI.CurrentProjection.StreamKernel.exists_seed_success line 71
4. lemma OAI.CurrentProjection.StreamKernel.completed_fixed_three_fifths line 90
5. theorem OAI.CurrentProjection.StreamKernel.streaming_three_fifths line 120
6. lemma OAI.CurrentProjection.StreamKernel.StreamingMain.mono line 134
7. lemma OAI.CurrentProjection.StreamKernel.three_fifths_le_two_thirds line 143
8. theorem OAI.CurrentProjection.criticalStreamingMain line 152
9. theorem OAI.CurrentProjection.levelsStreamingMain line 155
10. theorem OAI.CurrentProjection.hybridStreamingMain line 159
11. theorem OAI.CurrentProjection.fiberStreamingMain line 163