OAI/Combinatorics/Progressions/Estimates/NativeSelectedCorrelators.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.additiveQuadrupleCorrelation_support line 13
  2. theorem OAI.Erdos3.exists_many_correlated_additive_quadruples line 31
  3. theorem OAI.Erdos3.additiveQuadrupleCorrelation_real_scale line 97
  4. theorem OAI.Erdos3.derivative_quadruple_exp_threshold line 112
  5. theorem OAI.Erdos3.cross_correlations_force_additive_quadruples line 131
  6. theorem OAI.Erdos3.exists_many_cross_correlated_quadruples line 169
  7. theorem OAI.Erdos3.NativeCrossWitnesses.exists_quadruples line 243
  8. theorem OAI.Erdos3.NativeCrossWitnesses.exists_quadruples_budget line 301
  9. def OAI.Erdos3.NativeCrossWitnesses.restrict line 332
  10. theorem OAI.Erdos3.NativeCrossWitnesses.restrict_extension_of_mem line 335
  11. theorem OAI.Erdos3.NativeCrossWitnesses.restrict_quadruple line 340
  12. theorem OAI.Erdos3.NativeCrossWitnesses.exists_short_quadruples line 348
  13. theorem OAI.Erdos3.NativeCorrelationStructure.exists_bounded_correlator_quadruples line 393
  14. def OAI.Erdos3.NativeCorrelationStructure.selectedCorrelator line 420
  15. theorem OAI.Erdos3.NativeCorrelationStructure.selectedCorrelator_of_mem line 423
  16. theorem OAI.Erdos3.NativeCorrelationStructure.selectedCorrelator_of_not_mem line 427
  17. theorem OAI.Erdos3.NativeCorrelationStructure.boundedCorrelator_eq_scale line 431
  18. theorem OAI.Erdos3.NativeCorrelationStructure.boundedCorrelator_quadruple_scale line 439
  19. theorem OAI.Erdos3.NativeCorrelationStructure.exists_selected_correlator_quadruples line 450