OAI/Probability/SKBarriers/Locking/NarrowRetainedCommon.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SK.Analytic.vectorIncrementChain_div_scale line 15
2. theorem OAI.SK.Analytic.vectorIncrementAverage_div_scale line 23
3. def OAI.SK.Analytic.narrowCommonEmbedding line 33
4. theorem OAI.SK.Analytic.narrowCommonEmbedding_apply line 36
5. theorem OAI.SK.Analytic.narrowCommonBase_comp line 38
6. theorem OAI.SK.Analytic.narrowCommon_image line 45
7. theorem OAI.SK.Analytic.narrowRetainedCommon_value line 49
8. theorem OAI.SK.Analytic.narrowRetainedCommon_average line 57