OAI/Analysis/IrrationalRotation/Sampling/ScalarSamplingShear.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Invariant233.ScalarSampling.integrableOn_unitSquare_of_bound line 12
2. theorem OAI.Invariant233.ScalarSampling.double_interval_integral_shear line 21
3. theorem OAI.Invariant233.ScalarSampling.measurable_circleKernel line 41
4. lemma OAI.Invariant233.ScalarSampling.circleKernel_periodic_left line 59
5. lemma OAI.Invariant233.ScalarSampling.circleKernel_norm_le line 64
6. theorem OAI.Invariant233.ScalarSampling.endpoint_circleKernel_mass line 70
7. theorem OAI.Invariant233.ScalarSampling.endpoint_circleKernel_secondMoment line 78
8. theorem OAI.Invariant233.ScalarSampling.manuscriptEndpointKernel_mass line 93
9. theorem OAI.Invariant233.ScalarSampling.manuscriptEndpointKernel_secondMoment line 100