OAI/Combinatorics/Progressions/Estimates/QuarticCorrelatingVerticalPair.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.unit_vertical_frequency_integral_on_lattice line 19
  2. def OAI.Erdos3.cubicPairMiddleVerticalBudget line 36
  3. def OAI.Erdos3.NativePolynomialOrbitFactors.cubicPairMiddleFrequency line 50
  4. theorem OAI.Erdos3.NativePolynomialOrbitFactors.cubicPairMiddleFrequency_real line 55
  5. theorem OAI.Erdos3.NativePolynomialOrbitFactors.FrozenMiddleRealization.cubicPairMiddleFrequency_height line 80
  6. theorem OAI.Erdos3.NativePolynomialOrbitFactors.FrozenMiddleRealization.cubicPairMiddleFrequency_integral line 97
  7. def OAI.Erdos3.NativePolynomialOrbitFactors.FrozenMiddleRealization.cubicPairMiddleVertical line 108
  8. theorem OAI.Erdos3.NativePolynomialOrbitFactors.FrozenMiddleRealization.cubicPairMiddleVertical_eval line 141
  9. def OAI.Erdos3.quarticPairMiddleVerticalBudget line 166
  10. def OAI.Erdos3.NativePolynomialOrbitFactors.quarticPairMiddleFrequency line 180
  11. theorem OAI.Erdos3.NativePolynomialOrbitFactors.quarticPairMiddleFrequency_real line 185
  12. theorem OAI.Erdos3.NativePolynomialOrbitFactors.FrozenMiddleRealization.quarticPairMiddleFrequency_height line 210
  13. theorem OAI.Erdos3.NativePolynomialOrbitFactors.FrozenMiddleRealization.quarticPairMiddleTest_vertical line 227
  14. theorem OAI.Erdos3.NativePolynomialOrbitFactors.FrozenMiddleRealization.quarticPairMiddleFrequency_integral line 238
  15. def OAI.Erdos3.NativePolynomialOrbitFactors.FrozenMiddleRealization.quarticPairMiddleVertical line 246
  16. theorem OAI.Erdos3.NativePolynomialOrbitFactors.FrozenMiddleRealization.quarticPairMiddleVertical_eval line 277
  17. def OAI.Erdos3.NativePolynomialOrbitFactors.HasQuarticVerticalCorrelatingAnchor line 327
  18. theorem OAI.Erdos3.NativePolynomialOrbitFactors.hasQuarticVerticalCorrelatingAnchor_mono line 351
  19. theorem OAI.Erdos3.exists_quartic_correlating_vertical_pair line 363