OAI/Combinatorics/Progressions/Estimates/CubeSignalAlgebra.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.mixedCubeInput line 12
  2. def OAI.Erdos3.NativeMultidegreeNilcharacter.mixedCubeWithShift line 17
  3. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedCubeWithShift_unit line 24
  4. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedCubeWithShift_diagonal line 33
  5. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_mixed_cube_translation line 46
  6. def OAI.Erdos3.mixedCubeInputHom line 117
  7. def OAI.Erdos3.mixedCubeObservable line 139
  8. theorem OAI.Erdos3.mixedCubeObservable_unit line 143
  9. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedCubeWithShift_zero_eq line 150
  10. theorem OAI.Erdos3.NativeIntegerVectorEquivalence.exists_mixed_cube_budget line 158
  11. theorem OAI.Erdos3.mixedCubeObservable_norm_le_one line 183
  12. theorem OAI.Erdos3.conjugationPower_next_self line 193
  13. theorem OAI.Erdos3.norm_expect_conjugationPower line 198
  14. theorem OAI.Erdos3.cubeProduct_swap_head line 207
  15. theorem OAI.Erdos3.cubeProduct_comp_addHom line 212