OAI/Combinatorics/Progressions/Geometry/CertifiedFullChartDecompositionSource.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.NilpotentLieFiltration.FullChartMajorCorrelation line 14
2. theorem OAI.Erdos3.NilpotentLieFiltration.exists_full_chart_grade_correction_of_major_correlation line 55
3. def OAI.Erdos3.NilpotentLieFiltration.FullChartControlledFactors line 107
4. theorem OAI.Erdos3.NilpotentLieFiltration.FullChartControlledFactors.mono line 129
5. def OAI.Erdos3.NilpotentLieFiltration.FullChartControlledCorrelationSource line 143
6. def OAI.Erdos3.NilpotentLieFiltration.FullChartControlledCorrelationSourceStages line 175
7. theorem OAI.Erdos3.NilpotentLieFiltration.exists_bounded_full_chart_major_iteration line 218
8. structure OAI.Erdos3.NilpotentLieFiltration.FullChartMajorCorrelationWitness line 366
9. theorem OAI.Erdos3.NilpotentLieFiltration.exists_full_chart_grade_correction_of_major_correlation_witness line 396
10. def OAI.Erdos3.NilpotentLieFiltration.BundledFullChartControlledCorrelationSourceStages line 429
11. theorem OAI.Erdos3.NilpotentLieFiltration.exists_bounded_bundled_full_chart_major_iteration line 467
12. theorem OAI.Erdos3.NilpotentLieFiltration.exists_certified_full_chart_decomposition_of_major_correlation line 610
13. theorem OAI.Erdos3.NilpotentLieFiltration.exists_certified_full_chart_decomposition_of_major_correlation_witness line 654