OAI/NumberTheory/OrdinaryCorrelations/HighTrace/Avg.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OrdinaryCorrelations.FiniteIntegration.avg line 14
2. lemma OAI.OrdinaryCorrelations.FiniteIntegration.avg_nonneg line 17
3. lemma OAI.OrdinaryCorrelations.FiniteIntegration.avg_mono line 21
4. lemma OAI.OrdinaryCorrelations.FiniteIntegration.avg_const line 25
5. lemma OAI.OrdinaryCorrelations.FiniteIntegration.avg_mul_left line 30
6. lemma OAI.OrdinaryCorrelations.FiniteIntegration.avg_mul_right line 35
7. lemma OAI.OrdinaryCorrelations.FiniteIntegration.avg_prod line 40
8. lemma OAI.OrdinaryCorrelations.FiniteIntegration.avg_product line 46
9. lemma OAI.OrdinaryCorrelations.FiniteIntegration.abs_avg_le line 53
10. def OAI.OrdinaryCorrelations.FiniteIntegration.separatedKernel line 57
11. def OAI.OrdinaryCorrelations.FiniteIntegration.assignedIntegral line 62
12. theorem OAI.OrdinaryCorrelations.FiniteIntegration.assignedIntegral_signed line 69
13. theorem OAI.OrdinaryCorrelations.FiniteIntegration.assignedIntegral_le_product line 103
14. lemma OAI.OrdinaryCorrelations.FiniteIntegration.avg_equiv line 139