OAI/Combinatorics/Progressions/Fourier/CommonMarkedFrequencyModel.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.MultidegreeLieFiltration.exists_bounded_integral_model_with_frequency line 13
  2. theorem OAI.Erdos3.markedPolynomialValueHeight_le_exp line 55
  3. theorem OAI.Erdos3.markedQuotientFrequencyHeight_le_exp line 89
  4. theorem OAI.Erdos3.markedQuotientJointHeight_le_exp line 128
  5. def OAI.Erdos3.markedQuotientJointHeight line 154
  6. theorem OAI.Erdos3.exists_markedShift_integral_frequency_model line 167
  7. theorem OAI.Erdos3.integral_frequency_grid_allowance_le_exp line 223
  8. def OAI.Erdos3.markedFrequencyHeightBudget line 238
  9. def OAI.Erdos3.markedFrequencyModelBudget line 241
  10. theorem OAI.Erdos3.markedShiftInputBudget_le_frequencyHeight line 246
  11. theorem OAI.Erdos3.markedFrequencyHeightBudget_nonneg line 250
  12. theorem OAI.Erdos3.markedFrequencyHeightBudget_le_model line 254
  13. theorem OAI.Erdos3.exists_markedFrequencyModel_budget line 259
  14. theorem OAI.Erdos3.exists_markedShift_frequency_model_with_budget line 293
  15. theorem OAI.Erdos3.NativeRankRelation.CommonData.exists_native_marked_common_frequency_model line 379