OAI/Combinatorics/Progressions/Estimates/CubicAntisymmetricTransfer.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.RationalFilteredNilmanifold.topInvariant_integer_expansion_of_step line 15
  2. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.comparisonVerticalProduct_top_invariant line 55
  3. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.SymmetricSquarefreeUnitData.exists_nilcharacter line 127
  4. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.comparison_diagonal_expansion line 188
  5. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.comparison_diagonal_equivalence line 283
  6. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.exists_controlled_diagonal_comparison line 329
  7. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_factorial_diagonal line 441
  8. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_symmetric_multilinearization line 490
  9. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_symmetric_multilinearization_of_positive line 533
  10. abbrev OAI.Erdos3.CubicReplicatedIndex line 557
  11. def OAI.Erdos3.cubicLeftReplica line 559
  12. def OAI.Erdos3.cubicRightReplica line 561
  13. def OAI.Erdos3.cubicTrilinearInput line 563
  14. theorem OAI.Erdos3.cubicTrilinearInput_diagonal line 566
  15. def OAI.Erdos3.cubicTranslationInput line 574
  16. def OAI.Erdos3.cubicTranslationHom line 578
  17. theorem OAI.Erdos3.cubic_translated_input line 583
  18. theorem OAI.Erdos3.cubic_translation_expansion line 592
  19. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_cubic_translation_equivalence line 629
  20. theorem OAI.Erdos3.map_correlationInput line 704
  21. theorem OAI.Erdos3.NativeCorrelationStructure.mixed_correlation_transfer line 714
  22. theorem OAI.Erdos3.exists_multilinearized_correlation line 751
  23. theorem OAI.Erdos3.exists_absorb_global_cubic_error line 793
  24. def OAI.Erdos3.cubicFirstReplica line 856
  25. def OAI.Erdos3.cubicDiagonalCorner line 858
  26. def OAI.Erdos3.NativeMultidegreeNilcharacter.cubicDiagonalTensor line 872
  27. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicDiagonalTensor_norm line 875
  28. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicDiagonalTensor_unit line 880
  29. def OAI.Erdos3.NativeMultidegreeNilcharacter.cubicReflectionSource line 899
  30. def OAI.Erdos3.NativeMultidegreeNilcharacter.cubicReflectionTarget line 905
  31. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_cubic_reflected_factor_equivalence line 914
  32. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_cubic_reflected_pair_equivalence line 987
  33. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubic_reflection_target_unit line 1013
  34. theorem OAI.Erdos3.cubicTrilinearInput_reverse line 1036
  35. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.eval_cubicTrilinearInput_swap line 1047
  36. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_cubic_doubled_reflected_equivalence line 1066
  37. def OAI.Erdos3.NativeMultidegreeNilcharacter.cubicAntisymmetricPair line 1103
  38. theorem OAI.Erdos3.exists_cubic_antisymmetric_transfer line 1109