OAI/Combinatorics/Progressions/Linear/KernelJetAllowances.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.kernelJetInterpolationAllowance line 10
2. def OAI.Erdos3.kernelJetEntryAllowance line 13
3. def OAI.Erdos3.kernelJetMinorThreshold line 15
4. def OAI.Erdos3.kernelJetInverseAllowance line 18
5. theorem OAI.Erdos3.kernelJetInterpolationAllowance_pos line 22
6. theorem OAI.Erdos3.kernelJetEntryAllowance_pos line 27
7. theorem OAI.Erdos3.kernelJetMinorThreshold_pos line 31
8. theorem OAI.Erdos3.kernelJetInverseAllowance_nonneg line 37