OAI/Combinatorics/Progressions/Geometry/PreparedFullChartNativeDetection.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.NilpotentLieFiltration.exists_full_chart_major_correlation_witness_of_native_detections line 18
2. def OAI.Erdos3.VectorPolynomial.SampledSliceNativeDetection line 103
3. def OAI.Erdos3.VectorPolynomial.majorPhasePlateauBoxSignal line 124
4. theorem OAI.Erdos3.VectorPolynomial.majorPhasePlateauBoxSignal_inside line 132
5. theorem OAI.Erdos3.VectorPolynomial.majorPhasePlateauBoxSignal_outside line 141
6. theorem OAI.Erdos3.VectorPolynomial.majorPhasePlateauBoxSignal_norm_le_one line 150
7. theorem OAI.Erdos3.NilpotentLieFiltration.exists_full_chart_major_correlation_witness_of_prepared_detection line 170
8. theorem OAI.Erdos3.NilpotentLieFiltration.exists_full_chart_major_correlation_witness_of_productive_local_tests line 248
9. theorem OAI.Erdos3.NilpotentLieFiltration.exists_full_chart_major_correlation_witness_of_frozen_productive_local_tests line 355
10. theorem OAI.Erdos3.VectorPolynomial.preparedFullChartNativeDetection line 513