OAI/Probability/SKGap/Localization/CoordinateDeriv.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGap.coordinateDeriv line 13
2. lemma OAI.SKGap.lipschitz_insertNth line 17
3. lemma OAI.SKGap.continuous_insertNth_uncurry line 29
4. lemma OAI.SKGap.measurable_coordinateDeriv line 37
5. lemma OAI.SKGap.norm_coordinateDeriv_le line 49
6. theorem OAI.SKGap.gaussianProduct_lipschitz_IBP line 55
7. def OAI.SKGap.finiteCoordinateDeriv line 90
8. lemma OAI.SKGap.lipschitz_coordinate_update line 93
9. lemma OAI.SKGap.measurable_finiteCoordinateDeriv line 104
10. lemma OAI.SKGap.norm_finiteCoordinateDeriv_le line 110
11. lemma OAI.SKGap.gaussianFinite_lipschitz_IBP_equiv line 116
12. theorem OAI.SKGap.gaussianFinite_lipschitz_IBP line 152