OAI/NumberTheory/OrdinaryCorrelations/HighTrace/FreeSplit.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.freeSplit line 21
2. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.merge_freeSplit line 26
3. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.avg_residual_eq_split line 30
4. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.labelledIndicator_full_list line 38
5. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.allowedIndicator line 50
6. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.allowedIndicator_integer line 54
7. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.avoidance_eq_allowed line 68
8. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.retainedAllowedIntegral line 73
9. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.residualWitnessIntegral line 78
10. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.residualWitnessIntegral_nonneg line 83
11. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.avg_instance_congr line 92
12. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.assignedKernelIntegral_binary line 98
13. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.conditional_primitive_reduction line 112
14. theorem OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.primitive_cylinder_reduction line 133