OAI/Combinatorics/Progressions/Estimates/AllocatedExternalCandidatePrimitiveFrontDescentData.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.PositiveKernelPreparation.nativeQuotientIdeal line 43
2. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.PositiveKernelPreparation.nativeQuotientIdeal_terminal line 48
3. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.PositiveKernelPreparation.exists_native_descended_quotient line 53
4. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.PositiveKernelPreparation.exists_native_marked_descended_quotient line 187
5. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.CommonKeepPositiveKernelPreparation.exists_sourceProfile_spatialNativeFamily line 294
6. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.exists_primitive_sourceProfile_front line 415
7. structure OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.PrimitiveFrontQuotientData line 504
8. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.PrimitiveFrontQuotientData.family line 588
9. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.PrimitiveFrontQuotientData.family_eta line 592
10. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.PrimitiveFrontQuotientData.family_sourceChart line 596
11. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.PrimitiveFrontQuotientData.family_sourceCandidate line 598
12. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.PrimitiveFrontQuotientData.family_correlation line 600
13. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.PrimitiveFrontQuotientData.family_ideal line 604
14. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.exists_primitiveFrontQuotientData line 611
15. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.PrimitiveFrontQuotientData.factorFamily line 723
16. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.PrimitiveFrontQuotientData.factorFamily_eta line 727
17. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.PrimitiveFrontQuotientData.factorFamily_sourceChart line 731
18. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.PrimitiveFrontQuotientData.factorFamily_sourceCandidate line 734
19. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.PrimitiveFrontQuotientData.factorFamily_native line 737
20. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.PrimitiveFrontQuotientData.factorFamily_correlation line 740
21. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.PrimitiveFrontQuotientData.factorFamily_sourceChart_eq line 744
22. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.PrimitiveFrontQuotientData.factorFamily_sourceCandidate_heq line 748
23. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.PrimitiveFrontQuotientData.factorFamily_correlation_bound line 753
24. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.PrimitiveFrontQuotientData.factorFamily_path_eq line 757
25. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.PrimitiveFrontQuotientData.factorFamily_center_eq line 760
26. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.PrimitiveFrontQuotientData.factorFamily_score line 763
27. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.PrimitiveFrontQuotientData.frozen_side line 768
28. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.PrimitiveFrontQuotientData.source_geometry_bound line 778
29. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.PrimitiveFrontQuotientData.mark_geometry_bound line 782
30. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.PrimitiveFrontQuotientData.mark_height_bound line 787
31. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.PrimitiveFrontQuotientData.native_geometry_bound line 792
32. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.PrimitiveFrontQuotientData.pivot_card_bound line 796
33. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.PrimitiveFrontQuotientData.quotient_geometry_bound line 801
34. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.PrimitiveFrontQuotientData.quotient_projection_bound line 805
35. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.PrimitiveFrontQuotientData.factorFamily_quotient_filtration line 810
36. structure OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.PrimitiveFrontQuotientData.DescendedFamily line 867
37. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.PrimitiveFrontQuotientData.exists_descendedFamily line 898