OAI/NumberTheory/OrdinaryCorrelations/HighTrace/BetaZ.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OrdinaryCorrelations.SignedTrace.betaZ line 11
2. def OAI.OrdinaryCorrelations.SignedTrace.theta line 12
3. lemma OAI.OrdinaryCorrelations.SignedTrace.betaZ_value line 14
4. lemma OAI.OrdinaryCorrelations.SignedTrace.theta_value line 15
5. def OAI.OrdinaryCorrelations.SignedTrace.activeResidue line 19
6. def OAI.OrdinaryCorrelations.SignedTrace.departureCount line 21
7. def OAI.OrdinaryCorrelations.SignedTrace.centerPrimeFactor line 24
8. def OAI.OrdinaryCorrelations.SignedTrace.primeMean line 29
9. lemma OAI.OrdinaryCorrelations.SignedTrace.departureCount_sum line 31
10. lemma OAI.OrdinaryCorrelations.SignedTrace.normalization_product line 38
11. lemma OAI.OrdinaryCorrelations.SignedTrace.centerPrimeFactor_singleton line 45
12. lemma OAI.OrdinaryCorrelations.SignedTrace.singleton_mean_exact line 58
13. lemma OAI.OrdinaryCorrelations.SignedTrace.one_sub_normalization_nonneg line 94
14. lemma OAI.OrdinaryCorrelations.SignedTrace.one_sub_normalization_le_count line 97
15. theorem OAI.OrdinaryCorrelations.SignedTrace.source_good_singleton_integral line 105