OAI/NumberTheory/OrdinaryCorrelations/HighTrace/LocalIndicator.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification.localIndicator line 23
2. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification.jointIndicator line 25
3. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification.localIndicator_nonneg line 27
4. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification.jointIndicator_nonneg line 29
5. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification.jointIndicator_product line 31
6. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification.localIndicator_mean line 38
7. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification.jointIndicator_mean_le line 69
8. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.deletedIndicator line 87
9. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.deletedDensity line 89
10. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.deletedIndicator_integer_zero line 92
11. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.deletedDensity_le_majorant line 106