OAI/Combinatorics/Progressions/Estimates/OriginalMixedRootEquivalence.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.mixedSampledInput line 10
  2. theorem OAI.Erdos3.mixedSampledInput_slots line 14
  3. theorem OAI.Erdos3.mixedSampledInput_coordinates line 22
  4. theorem OAI.Erdos3.mixedSampledInput_map line 27
  5. def OAI.Erdos3.mixedPermuteSample line 32
  6. theorem OAI.Erdos3.mixedCoordinateIndex_coordinate line 46
  7. def OAI.Erdos3.mixedAllCoordinates line 52
  8. theorem OAI.Erdos3.mixedAllCoordinates_length line 55
  9. theorem OAI.Erdos3.mixedAllCoordinates_nodup line 58
  10. theorem OAI.Erdos3.mixedAllCoordinates_get line 62
  11. theorem OAI.Erdos3.mem_mixedAllCoordinates line 67
  12. def OAI.Erdos3.mixedCornerAssignmentEquiv line 72
  13. def OAI.Erdos3.mixedDiagonalCorner line 79
  14. theorem OAI.Erdos3.mixedDiagonalCorner_zero line 82
  15. def OAI.Erdos3.mixedDiagonalChoiceInput line 87
  16. theorem OAI.Erdos3.mixedDiagonalChoice_sum line 90
  17. theorem OAI.Erdos3.mixedDiagonalChoice_leaf line 99
  18. def OAI.Erdos3.NativeMultidegreeNilcharacter.mixedDiagonalTensor line 120
  19. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedDiagonalTensor_norm line 124
  20. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedDiagonalTensor_unit line 130
  21. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_mixed_diagonal_expansion line 149
  22. abbrev OAI.Erdos3.MixedNonconstantCorner line 189
  23. theorem OAI.Erdos3.mixedNonconstantCorner_card line 191
  24. def OAI.Erdos3.NativeMultidegreeNilcharacter.mixedDiagonalDerivative line 199
  25. def OAI.Erdos3.NativeMultidegreeNilcharacter.mixedNonconstantTensor line 203
  26. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedDiagonalDerivative_norm line 207
  27. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedNonconstantTensor_norm line 212
  28. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedDiagonalDerivative_unit line 217
  29. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedNonconstantTensor_unit line 222
  30. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_mixed_diagonal_derivative_equivalence line 230
  31. theorem OAI.Erdos3.mixedReplicated_totalDegree line 293
  32. def OAI.Erdos3.NativeMultidegreeNilcharacter.mixedPairComponent line 311
  33. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedPairComponent_eval line 318
  34. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedPairComponent_complexity line 325
  35. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedPairComponent_vertical line 328
  36. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedPairComponent_orbit_eq line 338
  37. def OAI.Erdos3.NativeMultidegreeNilcharacter.mixedIntegrationRoot line 353
  38. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedIntegrationRoot_dim line 359
  39. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_mixed_integration_root_equivalence line 363
  40. def OAI.Erdos3.NativeMultidegreeNilcharacter.mixedCyclicDiagonalDerivative line 424
  41. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedCyclicDiagonalDerivative_norm line 429
  42. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedCyclicDiagonalDerivative_unit line 435
  43. def OAI.Erdos3.NativeMultidegreeNilcharacter.mixedWrappedDiagonalDerivative line 441
  44. def OAI.Erdos3.NativeMultidegreeNilcharacter.mixedDiagonalWrapCoefficient line 445
  45. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedWrappedDiagonalDerivative_norm line 449
  46. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedDiagonalWrapCoefficient_norm line 454
  47. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedWrappedDiagonalDerivative_resolution line 459
  48. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedCyclicDiagonalDerivative_branches line 479
  49. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_mixedDiagonalWrapCoefficient_expansion line 498
  50. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_mixed_rational_division_equivalence line 530
  51. def OAI.Erdos3.mixedPairBudget line 563
  52. abbrev OAI.Erdos3.NativeSampleCorrelation.MixedPairAlgebra line 574
  53. def OAI.Erdos3.NativeSampleCorrelation.mixedPairModels line 576
  54. def OAI.Erdos3.NativeSampleCorrelation.mixedPairTests line 581
  55. def OAI.Erdos3.NativeSampleCorrelation.mixedPairFrequencies line 587
  56. theorem OAI.Erdos3.NativeSampleCorrelation.mixedPairTests_eval line 592
  57. theorem OAI.Erdos3.NativeSampleCorrelation.mixedPairTests_vertical line 607
  58. theorem OAI.Erdos3.NativeSampleCorrelation.mixedPairBudget_six_le line 625
  59. theorem OAI.Erdos3.NativeSampleCorrelation.mixedPairTests_complexity line 631
  60. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_original_mixed_root_equivalence line 661