OAI/Combinatorics/Progressions/Estimates/FreeCorrelationRelationRefinement.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.NativeRankRelation.CommonData.realCoefficientFourSpace line 23
  2. theorem OAI.Erdos3.NativeRankRelation.CommonData.real_coefficient_four_tensor_frequency line 28
  3. theorem OAI.Erdos3.NativeRankRelation.CommonData.real_coefficient_four_frequency line 71
  4. theorem OAI.Erdos3.NativeRankRelation.CommonData.mem_real_coefficientFourSpace line 112
  5. theorem OAI.Erdos3.NativeRankRelation.CommonData.CoefficientBases.finite_combined_free_sunflower line 152
  6. theorem OAI.Erdos3.NativeRankRelation.CommonData.CoefficientBases.real_finite_combined_free_sunflower line 175
  7. theorem OAI.Erdos3.NativeRankRelation.CommonData.CoefficientBases.exists_free_tree_linearization line 200
  8. theorem OAI.Erdos3.NativeRankRelation.CommonData.CoefficientBases.exists_real_free_tree_linearization line 218
  9. theorem OAI.Erdos3.NativeRankRelation.CommonData.CoefficientBases.free_refined_four_identity line 262
  10. theorem OAI.Erdos3.NativeRankRelation.CommonData.CoefficientBases.real_free_refined_four_identity line 275
  11. theorem OAI.Erdos3.NativeRankRelation.CommonData.CoefficientBases.free_refined_petal_vanish line 288
  12. theorem OAI.Erdos3.NativeRankRelation.CommonData.CoefficientBases.real_free_refined_petal_vanish line 307
  13. theorem OAI.Erdos3.NativeRankRelation.CommonData.CoefficientBases.correlation_four_frequency line 365
  14. theorem OAI.Erdos3.NativeRankRelation.CommonData.CoefficientBases.real_correlation_four_frequency line 376
  15. theorem OAI.Erdos3.NativeRankRelation.CommonData.CoefficientBases.correlation_refined_four_identity line 387
  16. theorem OAI.Erdos3.NativeRankRelation.CommonData.CoefficientBases.real_correlation_refined_four_identity line 397
  17. theorem OAI.Erdos3.NativeRankRelation.CommonData.CoefficientBases.correlation_refined_petal_vanish line 408
  18. theorem OAI.Erdos3.NativeRankRelation.CommonData.CoefficientBases.real_correlation_refined_petal_vanish line 423