OAI/Probability/SKGap/Localization/CyclicPrediction.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.SKGap.Noncrossing.mean_finset_sumline 14 - lemma
OAI.SKGap.Noncrossing.ordinary_mean_noise_rotateline 19 - lemma
OAI.SKGap.Noncrossing.ordinary_mean_cons_rotateline 31 - theorem
OAI.SKGap.Noncrossing.ordinary_mean_cyclicline 37 - lemma
OAI.SKGap.Noncrossing.meanSeries_cyclicline 45 - theorem
OAI.SKGap.Noncrossing.wordPrediction_mean_cyclicline 66