OAI/Probability/SKGap/Localization/DimensionDecayPos.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGapCutoff.dimensionDecay_pos line 146
2. lemma OAI.SKGapCutoff.dimensionDecay_le_one line 148
3. lemma OAI.SKGapCutoff.dimensionDecay_mul line 154
4. lemma OAI.SKGapCutoff.nat_mul_dimensionDecay line 161
5. lemma OAI.SKGapCutoff.nat_sq_mul_dimensionDecay line 165
6. lemma OAI.SKGapCutoff.exp_cutoffTime_eq_dimensionDecay line 171
7. lemma OAI.SKGapCutoff.dimensionDecay_mul_cutoffTime_tendsto line 177
8. lemma OAI.SKGapCutoff.linear_mean_error_tendsto line 189
9. lemma OAI.SKGapCutoff.upper_polynomial_error_tendsto line 196