OAI/NumberTheory/OrdinaryCorrelations/HighTrace/AvgAdd.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OrdinaryCorrelations.SourceCylinder.avg_add' line 19
2. lemma OAI.OrdinaryCorrelations.SourceCylinder.avg_sub' line 23
3. lemma OAI.OrdinaryCorrelations.SourceCylinder.avg_sum' line 27
4. lemma OAI.OrdinaryCorrelations.SourceCylinder.avg_ite_add_sum_mul line 32
5. lemma OAI.OrdinaryCorrelations.SourceCylinder.truncated_real line 47
6. theorem OAI.OrdinaryCorrelations.SourceCylinder.signed_list_reduction line 56