OAI/Combinatorics/Progressions/Estimates/NativeMultilinearityCorrelation.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.coordinateSumVector line 14
  2. def OAI.Erdos3.coordinateTensorVector line 18
  3. theorem OAI.Erdos3.coordinateAdditionProduct_eq line 22
  4. theorem OAI.Erdos3.coordinateSumVector_unit line 28
  5. theorem OAI.Erdos3.coordinateTensorVector_unit line 32
  6. theorem OAI.Erdos3.NativeIntegerVectorEquivalence.of_addition_family line 46
  7. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.exists_controlled_addition_model line 83
  8. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.exists_controlled_addition_family line 125
  9. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_addition_family line 193
  10. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_addition_equivalence line 218
  11. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_multilinearity_equivalence line 240
  12. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_multilinearity_cyclic_equivalence line 255
  13. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_multilinearity_transfer_budget line 277