OAI/Combinatorics/Progressions/Polynomial/DegreeRankNativeInverseModels.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.Erdos3.NativeDegreeRankDerivativeData line 15
2. def OAI.Erdos3.NativeDegreeRankDerivativeData.mono line 27
3. theorem OAI.Erdos3.NativeDegreeRankDerivativeData.rank_vertical line 34
4. theorem OAI.Erdos3.NativeDegreeRankDerivativeData.rank_integral line 41
5. theorem OAI.Erdos3.NativeDegreeRankDerivativeData.rank_orbit_normalized line 45
6. theorem OAI.Erdos3.NativeDegreeRankDerivativeData.rank_correlation line 51
7. theorem OAI.Erdos3.exists_degree_rank_native_inverse_models line 73