OAI/Combinatorics/Progressions/Estimates/CubicRootPermutation.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.NativeMultidegreeNilcharacter.cubicPairComponent line 20
  2. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicPairComponent_eval line 26
  3. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicPairComponent_complexity line 53
  4. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicPairComponent_vertical line 58
  5. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicPairComponent_orbit_eq line 71
  6. def OAI.Erdos3.NativeMultidegreeNilcharacter.cubicOriginalComponent line 93
  7. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicOriginalComponent_eval line 99
  8. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicOriginalComponent_complexity line 118
  9. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicOriginalComponent_vertical line 123
  10. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicOriginalComponent_orbit_pair line 136
  11. def OAI.Erdos3.cubicPairBudget line 159
  12. abbrev OAI.Erdos3.NativeSampleCorrelation.CubicPairAlgebra line 170
  13. def OAI.Erdos3.NativeSampleCorrelation.cubicPairModels line 172
  14. def OAI.Erdos3.NativeSampleCorrelation.cubicPairTests line 177
  15. def OAI.Erdos3.NativeSampleCorrelation.cubicPairFrequencies line 183
  16. theorem OAI.Erdos3.NativeSampleCorrelation.cubicPairTests_eval line 188
  17. theorem OAI.Erdos3.NativeSampleCorrelation.cubicPairTests_vertical line 200
  18. theorem OAI.Erdos3.NativeSampleCorrelation.cubicPairBudget_six_le line 218
  19. theorem OAI.Erdos3.NativeSampleCorrelation.cubicPairTests_complexity line 224
  20. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_cubic_integer_translation_equivalence line 260
  21. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_cubic_shifted_diagonal_equivalence line 299
  22. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_cubic_mixed_shifted_equivalence line 324
  23. def OAI.Erdos3.NativeMultidegreeNilcharacter.cubicRoot line 361
  24. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicRoot_dim line 366
  25. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_explicit_cubic_root_equivalence line 370
  26. def OAI.Erdos3.NativeMultidegreeNilcharacter.cubicCyclicDiagonalDerivative line 428
  27. def OAI.Erdos3.NativeMultidegreeNilcharacter.cubicWrappedDiagonalDerivative line 433
  28. def OAI.Erdos3.NativeMultidegreeNilcharacter.cubicDiagonalWrapCoefficient line 437
  29. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicWrappedDiagonalDerivative_norm line 441
  30. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicDiagonalWrapCoefficient_norm line 447
  31. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicWrappedDiagonalDerivative_resolution line 453
  32. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicCyclicDiagonalDerivative_branches line 473
  33. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_cubicDiagonalWrapCoefficient_expansion line 492
  34. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.third_dilation_integer_representative line 529
  35. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_cubic_third_dilation_pattern_equivalence line 541
  36. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_third_dilation_last_slots_equivalence line 645
  37. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_cubic_root_last_slots_equivalence line 677