OAI/Analysis/FourierLLogL/Fourier/Scale.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FourierLLogL.Period.scales line 13
2. def OAI.FourierLLogL.Period.averageH line 15
3. def OAI.FourierLLogL.Period.convK line 18
4. lemma OAI.FourierLLogL.Period.seg_integral_slices line 21
5. lemma OAI.FourierLLogL.Period.measurable_layer line 32
6. lemma OAI.FourierLLogL.Period.inv_sq_bound line 39
7. lemma OAI.FourierLLogL.Period.weight_bound line 46
8. instance OAI.FourierLLogL.Period.scales_fin line 52
9. instance OAI.FourierLLogL.Period.origins_fin line 55
10. instance OAI.FourierLLogL.Period.window_fin line 58
11. lemma OAI.FourierLLogL.Period.average_succ line 61
12. def OAI.FourierLLogL.Period.portion line 94
13. lemma OAI.FourierLLogL.Period.scale_subst line 96
14. lemma OAI.FourierLLogL.Period.kernel_split line 118
15. lemma OAI.FourierLLogL.Period.convolution_average line 133
16. def OAI.FourierLLogL.Period.maxConvK line 192
17. lemma OAI.FourierLLogL.Period.measurable_maxConvK line 195
18. lemma OAI.FourierLLogL.Period.convolution_cost line 205