OAI/NumberTheory/PrimePackets/AdelicAveraging.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.PrimeDegreePackets.Adelic.PacketTorusParametrization line 13
2. lemma OAI.PrimeDegreePackets.Adelic.PacketTorusParametrization.period_eq line 30
3. lemma OAI.PrimeDegreePackets.Adelic.PacketTorusParametrization.exists_basepoint_lift line 40
4. def OAI.PrimeDegreePackets.Adelic.PacketTorusParametrization.select line 47
5. lemma OAI.PrimeDegreePackets.Adelic.PacketTorusParametrization.select_eq line 49
6. lemma OAI.PrimeDegreePackets.Adelic.PacketTorusParametrization.point_orbit_mem line 52
7. def OAI.PrimeDegreePackets.Adelic.PacketTorusParametrization.orbitTranslate line 60
8. lemma OAI.PrimeDegreePackets.Adelic.PacketTorusParametrization.orbitTranslate_injective line 63
9. lemma OAI.PrimeDegreePackets.Adelic.PacketTorusParametrization.basepoint_period_eq line 77
10. lemma OAI.PrimeDegreePackets.Adelic.PacketTorusParametrization.basepoint_volume_eq line 82
11. lemma OAI.PrimeDegreePackets.Adelic.PacketTorusParametrization.point_period_eq_basepoint line 87
12. lemma OAI.PrimeDegreePackets.Adelic.PacketTorusParametrization.packetMeasure_eq_uniform line 92
13. lemma OAI.PrimeDegreePackets.Adelic.PacketTorusParametrization.sum_translated_orbitProbabilities line 104
14. lemma OAI.PrimeDegreePackets.Adelic.PacketTorusParametrization.exists_common_average line 116