OAI/Combinatorics/Progressions/Estimates/AllocatedPrimitiveFrontInitialLong.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.allocatedCandidate_initialLong_excluded_bound line 11
2. theorem OAI.Erdos3.VectorPolynomial.allocatedCandidate_retainedMass_pos line 25
3. abbrev OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.InnerSourceProfile.stageKeep line 51
4. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.InnerSourceProfile.stageKeep_kept line 57
5. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.InnerSourceProfile.stageKeep_frozen line 65
6. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.InnerSourceProfile.stageKeep_subset_initialLong line 74
7. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.InnerSourceProfile.detectionLoss_le_retainedMass line 85
8. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.InnerSourceProfile.detectionLoss_le_spatialNativeMass line 103
9. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.InnerSourceProfile.markHeight_bounds line 113
10. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.PrimitiveFrontQuotientData.retained_nonempty line 165
11. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.PrimitiveFrontQuotientData.initialLong_nonempty line 172
12. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.PrimitiveFrontQuotientData.initialLong_excluded_bound line 186
13. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.PrimitiveFrontQuotientData.initialLong_excluded_bound_of_cost_le line 193