OAI/Combinatorics/Progressions/Estimates/ProductRestrictionWeightedCommonFactors.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.RationalFilteredNilmanifold.productRestriction_jointOrbitSymbol line 22
  2. def OAI.Erdos3.RationalFilteredNilmanifold.productRestrictionSectionLinear line 59
  3. theorem OAI.Erdos3.RationalFilteredNilmanifold.productRestrictionSectionLinear_apply line 64
  4. theorem OAI.Erdos3.RationalFilteredNilmanifold.productRestrictionSectionLinear_apply_of_not_mem line 76
  5. def OAI.Erdos3.RationalFilteredNilmanifold.productRestrictionSection line 86
  6. theorem OAI.Erdos3.RationalFilteredNilmanifold.productRestrictionSection_apply line 98
  7. theorem OAI.Erdos3.RationalFilteredNilmanifold.productRestrictionSection_apply_of_not_mem line 103
  8. theorem OAI.Erdos3.RationalFilteredNilmanifold.productRestrictionSection_rightInverse line 108
  9. theorem OAI.Erdos3.RationalFilteredNilmanifold.productRestrictionSection_layers line 119
  10. theorem OAI.Erdos3.RationalFilteredNilmanifold.productRestrictionSection_coordinates line 131
  11. theorem OAI.Erdos3.RationalFilteredNilmanifold.productRestrictionSection_coordinates_of_not_mem line 138
  12. theorem OAI.Erdos3.RationalFilteredNilmanifold.productRestriction_layer_surjective line 147
  13. theorem OAI.Erdos3.RationalFilteredNilmanifold.productRestriction_matrix_height line 164
  14. theorem OAI.Erdos3.RationalFilteredNilmanifold.productRestriction_adapted_matrix_logHeight line 178
  15. theorem OAI.Erdos3.RationalFilteredNilmanifold.productRestriction_controlledSymbolFactorizationAtFast line 211
  16. theorem OAI.Erdos3.RationalFilteredNilmanifold.productRestriction_controlledSymbolFactorization line 242
  17. theorem OAI.Erdos3.RationalFilteredNilmanifold.productRestriction_jointOrbit_controlledSymbolFactorization line 270
  18. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_productRestriction_jointOrbit_controlledSymbolFactorizationAtFast line 310
  19. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_productRestriction_jointOrbit_controlledSymbolFactorization line 356
  20. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_productRestriction_weighted_common_orbit_factors line 404