OAI/Analysis/IrrationalRotation/Sampling/CharacterSamplingLp.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Invariant233.CharacterSampling.measurable_average line 16
2. theorem OAI.Invariant233.CharacterSampling.memLp_samplingError_comp line 28
3. theorem OAI.Invariant233.CharacterSampling.tendsto_eLpNorm_samplingError line 45
4. theorem OAI.Invariant233.CharacterSampling.eventually_eLpNorm_samplingError_lt line 79