OAI/Combinatorics/Progressions/Estimates/QuadraticPairCorrelator.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_antisymmetric_anchor_expansion line 9
  2. def OAI.Erdos3.NativeIntegerExpansion.boxSlice line 60
  3. theorem OAI.Erdos3.exists_antisymmetric_pair_approximation line 74
  4. theorem OAI.Erdos3.exists_antisymmetric_pair_correlation line 137
  5. def OAI.Erdos3.NativeMultidegreeNilcharacter.pairComponent line 190
  6. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.pairComponent_eval line 196
  7. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.pairComponent_vertical line 203
  8. def OAI.Erdos3.antisymmetricPairBudget line 215
  9. abbrev OAI.Erdos3.NativeSampleCorrelation.AntisymmetricPairAlgebra line 225
  10. def OAI.Erdos3.NativeSampleCorrelation.antisymmetricPairModels line 228
  11. def OAI.Erdos3.NativeSampleCorrelation.antisymmetricPairTests line 233
  12. def OAI.Erdos3.NativeSampleCorrelation.antisymmetricPairFrequencies line 238
  13. theorem OAI.Erdos3.NativeSampleCorrelation.antisymmetricPairTests_eval line 243
  14. theorem OAI.Erdos3.NativeSampleCorrelation.antisymmetricPairTests_vertical line 254
  15. theorem OAI.Erdos3.NativeSampleCorrelation.antisymmetricPairBudget_four_le line 273
  16. theorem OAI.Erdos3.NativeSampleCorrelation.antisymmetricPairTests_complexity line 279
  17. theorem OAI.Erdos3.exists_quadratic_pair_correlator line 310