OAI/Probability/SKBarriers/Hierarchy/WeightedListBridge.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SK.Analytic.vectorStepAverage_frozen line 15
2. def OAI.SK.Analytic.zeroWeightChain line 25
3. def OAI.SK.Analytic.zeroNoiseEmbedding line 27
4. theorem OAI.SK.Analytic.zeroNoiseEmbedding_apply line 29
5. theorem OAI.SK.Analytic.weightedUnderlying_zeroWeight line 31
6. theorem OAI.SK.Analytic.weightedUnderlying_append line 35
7. theorem OAI.SK.Analytic.zeroWeightChain_average line 39
8. theorem OAI.SK.Analytic.weightedFull_average line 51