OAI/Probability/StrongRayleigh/GroupDrift.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem336AdditiveD139.groupDrift line 14
2. theorem OAI.Problem336AdditiveD139.groupDrift_eq_finiteFieldMean_limsup line 19
3. theorem OAI.Problem336AdditiveD139.measurable_groupDrift line 26
4. theorem OAI.Problem336AdditiveD139.groupDrift_mem_Icc line 35
5. theorem OAI.Problem336AdditiveD139.groupDrift_response_of_finite_response line 43
6. theorem OAI.Problem336AdditiveD139.groupDrift_translate line 67
7. theorem OAI.Problem336AdditiveD139.groupDrift_leftTranslate line 79
8. theorem OAI.Problem336AdditiveD139.groupDrift_zero_zero line 88