OAI/Combinatorics/Progressions/Geometry/QuarticBoxStepDrop.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Erdos3.QuarticBoxIndex line 10
  2. def OAI.Erdos3.NativeMultidegreeNilcharacter.quarticBoxComponent line 23
  3. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticBoxComponent_eval line 29
  4. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticBoxComponent_vertical line 40
  5. def OAI.Erdos3.NativeMultidegreeNilcharacter.quarticKernelFactors line 50
  6. def OAI.Erdos3.NativeMultidegreeNilcharacter.quarticKernelFrequencies line 54
  7. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticKernelFactors_complexity line 57
  8. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticKernelFactors_normBound line 65
  9. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticKernelFactors_eval line 69
  10. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticKernelFactors_vertical line 75
  11. abbrev OAI.Erdos3.QuarticBoxFactor line 97
  12. theorem OAI.Erdos3.quarticBoxFactor_card line 99
  13. def OAI.Erdos3.quarticBoxCorner line 101
  14. def OAI.Erdos3.NativeMultidegreeNilcharacter.quarticAntisymmetricBoxValue line 114
  15. def OAI.Erdos3.NativeMultidegreeNilcharacter.quarticAntisymmetricBoxFactors line 117
  16. def OAI.Erdos3.NativeMultidegreeNilcharacter.quarticAntisymmetricBoxFrequencies line 122
  17. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticAntisymmetricBoxFactors_complexity line 125
  18. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticAntisymmetricBoxFactors_normBound line 130
  19. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticAntisymmetricBoxFactors_eval line 135
  20. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticAntisymmetricBoxValue_norm line 151
  21. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticAntisymmetricBoxFactors_vertical line 159
  22. def OAI.Erdos3.NativeMultidegreeNilcharacter.quarticAntisymmetricBoxNiltest line 177
  23. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticAntisymmetricBoxNiltest_complexity line 184
  24. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticAntisymmetricBoxNiltest_eval line 191
  25. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticAntisymmetricBoxNiltest_vertical line 197
  26. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticAntisymmetricBoxValue_mean line 230
  27. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticAntisymmetricBoxNiltest_mean line 240
  28. structure OAI.Erdos3.NativeQuarticBoxFactorization line 262
  29. theorem OAI.Erdos3.exists_quartic_box_step_drop_indices line 282