OAI/Probability/Renewal/Fourier.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HoneycombLocal.latticeChar line 10
2. lemma OAI.HoneycombLocal.integrable_lattice_exp line 13
3. lemma OAI.HoneycombLocal.latticeChar_eq_charFun line 18
4. lemma OAI.HoneycombLocal.norm_latticeChar_le_one line 24
5. lemma OAI.HoneycombLocal.continuous_latticeChar line 28
6. lemma OAI.HoneycombLocal.integral_lattice_exp line 34
7. lemma OAI.HoneycombLocal.lattice_inversion line 59
8. lemma OAI.HoneycombLocal.two_copy_defect line 99
9. lemma OAI.HoneycombLocal.integrable_two_copy_defect line 137
10. lemma OAI.HoneycombLocal.rectangle_defect_bound line 145
11. lemma OAI.HoneycombLocal.support_diff_cos_eq_one line 163
12. lemma OAI.HoneycombLocal.exp_of_cos_eq_one line 176
13. lemma OAI.HoneycombLocal.norm_latticeChar_lt_one line 185
14. lemma OAI.HoneycombLocal.lattice_spectral_gap line 217