OAI/Combinatorics/Progressions/Estimates/PositiveShiftProductData.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.anchoredInputs line 14
  2. theorem OAI.Erdos3.anchoredInputs_prod line 18
  3. def OAI.Erdos3.RationalFilteredNilmanifold.anchoredReferenceData line 35
  4. def OAI.Erdos3.RationalFilteredNilmanifold.anchoredObservableData line 44
  5. def OAI.Erdos3.RationalFilteredNilmanifold.anchoredFrequencyData line 53
  6. theorem OAI.Erdos3.RationalFilteredNilmanifold.anchoredObservableData_product line 62
  7. def OAI.Erdos3.anchoredOptionInputs line 82
  8. theorem OAI.Erdos3.anchoredOptionInputs_prod line 86
  9. def OAI.Erdos3.RationalFilteredNilmanifold.anchoredOptionReferenceData line 100
  10. def OAI.Erdos3.RationalFilteredNilmanifold.anchoredOptionObservableData line 109
  11. def OAI.Erdos3.RationalFilteredNilmanifold.anchoredOptionFrequencyData line 118
  12. theorem OAI.Erdos3.RationalFilteredNilmanifold.anchoredOptionObservableData_product line 127
  13. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_anchored_product_family line 154
  14. abbrev OAI.Erdos3.PositiveShiftBasis.anchoredLieSpace line 269
  15. abbrev OAI.Erdos3.PositiveShiftBasis.anchoredDimension line 272
  16. def OAI.Erdos3.PositiveShiftBasis.anchoredFactors line 281
  17. theorem OAI.Erdos3.PositiveShiftBasis.anchoredFactors_geometry line 285
  18. def OAI.Erdos3.PositiveShiftBasis.anchoredWeights line 295
  19. theorem OAI.Erdos3.PositiveShiftBasis.anchoredFactors_layers line 302