OAI/Combinatorics/Progressions/Sampling/TranslatedPartialPeriodicGridIntegrability.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Erdos3.partialPeriodicIntegerGrid_integrableline 15 - theorem
OAI.Erdos3.partialPeriodicResidueIntegral_integrableline 50 - theorem
OAI.Erdos3.integral_partialPeriodicGrid_sub_referenceline 67 - theorem
OAI.Erdos3.translatedPartialPeriodicIntegerGrid_integrableline 96 - theorem
OAI.Erdos3.integral_translatedPartialPeriodicGrid_sub_referenceline 131