OAI/Probability/SKGap/Localization/MarkedProductIBP.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGap.scalar_bounded_product_lipschitz line 12
2. theorem OAI.SKGap.goe_marked_product_IBP line 34
3. lemma OAI.SKGap.marked_entry_bound line 93
4. theorem OAI.SKGap.projected_marked_expectation_error line 109