OAI/Combinatorics/Progressions/Estimates/QuarticPairPartitionedModel.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.NativeSampleCorrelation.normalized_reverse_correlation line 19
  2. theorem OAI.Erdos3.NativeCubicPairPartition.exists_witness_cell line 52
  3. theorem OAI.Erdos3.exists_cubic_pair_partition line 65
  4. theorem OAI.Erdos3.exists_cubic_pair_witness_partition line 112
  5. theorem OAI.Erdos3.exists_cubic_pair_partitioned_model line 156
  6. theorem OAI.Erdos3.exists_quartic_pair_factored_model line 241
  7. structure OAI.Erdos3.QuarticMixedRowData line 329
  8. def OAI.Erdos3.QuarticMixedRowData.row line 345
  9. theorem OAI.Erdos3.QuarticMixedRowData.row_norm line 349
  10. theorem OAI.Erdos3.QuarticMixedRowData.row_correlation line 353
  11. theorem OAI.Erdos3.QuarticMixedRowData.row_mass line 361
  12. def OAI.Erdos3.QuarticMixedRowData.mono line 383
  13. theorem OAI.Erdos3.exists_quartic_mixed_row_data line 391
  14. theorem OAI.Erdos3.NativeQuarticPairPartition.exists_witness_cell line 452
  15. theorem OAI.Erdos3.exists_quartic_pair_partition line 465
  16. theorem OAI.Erdos3.exists_quartic_pair_witness_partition line 513
  17. theorem OAI.Erdos3.exists_quartic_pair_partitioned_model line 558