OAI/Analysis/IrrationalRotation/Sampling/CircleSamplingLp.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.CircleParameterData.kernel_bounds line 11
2. theorem OAI.Invariant233.CircleParameterData.orientedKernel_bounds line 28
3. theorem OAI.Invariant233.CircleParameterData.samplingAverage_bounds line 35
4. theorem OAI.Invariant233.CircleParameterData.memLp_samplingAverage line 73
5. theorem OAI.Invariant233.CircleParameterData.memLp_samplingError line 86