OAI/Probability/SKGap/Localization/DimensionDecay.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGapCutoff.dimensionDecay line 11
2. lemma OAI.SKGapCutoff.dimensionDecay_tendsto line 14
3. lemma OAI.SKGapCutoff.dimensionDecay_upper_tendsto line 22
4. lemma OAI.SKGapCutoff.mul_exp_log_identity line 29
5. lemma OAI.SKGapCutoff.exp_log_div_identity line 37
6. lemma OAI.SKGapCutoff.cutoffTime_one line 45
7. lemma OAI.SKGapCutoff.cutoffTime_one_nonneg line 48
8. lemma OAI.SKGapCutoff.tendsto_one_of_error line 52
9. lemma OAI.SKGapCutoff.continuous_zero_cutoff_upper line 61
10. lemma OAI.SKGapCutoff.continuous_zero_cutoff_lower line 80
11. lemma OAI.SKGapCutoff.sampledInteraction_zero line 98
12. lemma OAI.SKGapCutoff.disorderLaw_zero line 103
13. lemma OAI.SKGapCutoff.disorderLimit_zero_of_tendsto line 123
14. lemma OAI.SKGapCutoff.discrete_zero_cutoff_upper line 136
15. lemma OAI.SKGapCutoff.discrete_zero_cutoff_lower line 155
16. theorem OAI.SKGapCutoff.beta_zero_cutoff line 185