OAI/Combinatorics/Progressions/Estimates/QuarticPairFactors.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.NativeMultidegreeNilcharacter.quarticPairComponent line 18
  2. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticPairComponent_eval line 24
  3. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticPairComponent_complexity line 35
  4. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticPairComponent_vertical line 38
  5. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticPairComponent_orbit_eq line 48
  6. def OAI.Erdos3.quarticPairBudget line 69
  7. abbrev OAI.Erdos3.NativeSampleCorrelation.QuarticPairAlgebra line 80
  8. def OAI.Erdos3.NativeSampleCorrelation.quarticPairModels line 82
  9. def OAI.Erdos3.NativeSampleCorrelation.quarticPairTests line 87
  10. def OAI.Erdos3.NativeSampleCorrelation.quarticPairFrequencies line 93
  11. theorem OAI.Erdos3.NativeSampleCorrelation.quarticPairTests_eval line 98
  12. theorem OAI.Erdos3.NativeSampleCorrelation.quarticPairTests_vertical line 114
  13. theorem OAI.Erdos3.NativeSampleCorrelation.quarticPairBudget_six_le line 132
  14. theorem OAI.Erdos3.NativeSampleCorrelation.quarticPairTests_complexity line 138