OAI/Analysis/IrrationalRotation/Sampling/CircleDigitEnergy.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Invariant233.CircleDigitCoupling.endpointDensity_memLp line 13
2. lemma OAI.Invariant233.CircleDigitCoupling.marginalDensity_memLp line 19
3. lemma OAI.Invariant233.CircleDigitCoupling.endpointDensity_integral line 25
4. lemma OAI.Invariant233.CircleDigitCoupling.marginalDensity_integral line 40
5. lemma OAI.Invariant233.CircleDigitCoupling.marginalDensity_energy line 57
6. lemma OAI.Invariant233.CircleDigitCoupling.rawLaw_map_endpoint line 110