OAI/Probability/MemoryPrecision/LabelTranslations.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MemoryPrecision.labelTranslate line 22
2. lemma OAI.MemoryPrecision.measurePreserving_labelTranslate line 26
3. lemma OAI.MemoryPrecision.continuous_labelTranslate line 32
4. lemma OAI.MemoryPrecision.tendsto_eLpNorm_labelTranslate_sub line 39
5. lemma OAI.MemoryPrecision.eLpNorm_labelTranslate_sub_le line 66
6. def OAI.MemoryPrecision.averageTranslate line 75
7. lemma OAI.MemoryPrecision.integrable_translate_product line 80
8. lemma OAI.MemoryPrecision.eLpNorm_averageTranslate_sub_le line 98
9. lemma OAI.MemoryPrecision.tendsto_eLpNorm_averageTranslate_sub line 125