OAI/Combinatorics/Progressions/FixedDensity/SimplexTelescoping.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Erdos3.FixedDensity.DeletedVector line 12
  2. def OAI.Erdos3.FixedDensity.deleteCoordinate line 15
  3. structure OAI.Erdos3.FixedDensity.WeightedSimplexSystem line 20
  4. def OAI.Erdos3.FixedDensity.WeightedSimplexSystem.simplexWeight line 25
  5. def OAI.Erdos3.FixedDensity.WeightedSimplexSystem.simplexCount line 29
  6. theorem OAI.Erdos3.FixedDensity.WeightedSimplexSystem.simplexWeight_nonneg line 33
  7. theorem OAI.Erdos3.FixedDensity.WeightedSimplexSystem.simplexCount_nonneg line 40
  8. theorem OAI.Erdos3.FixedDensity.WeightedSimplexSystem.simplexWeight_mono line 47
  9. theorem OAI.Erdos3.FixedDensity.WeightedSimplexSystem.simplexCount_mono line 57
  10. def OAI.Erdos3.FixedDensity.apSimplexForm line 67
  11. def OAI.Erdos3.FixedDensity.simplexCoordinateSum line 72
  12. def OAI.Erdos3.FixedDensity.simplexCoordinateMoment line 76
  13. theorem OAI.Erdos3.FixedDensity.apSimplexForm_deleteCoordinate line 80
  14. def OAI.Erdos3.FixedDensity.apSimplexSystem line 111
  15. theorem OAI.Erdos3.FixedDensity.apSimplexSystem_simplexWeight line 115
  16. def OAI.Erdos3.FixedDensity.simplexTailSum line 144
  17. def OAI.Erdos3.FixedDensity.simplexTailMoment line 147
  18. def OAI.Erdos3.FixedDensity.simplexCoordinatesOfAP line 150
  19. theorem OAI.Erdos3.FixedDensity.simplexCoordinatesOfAP_zero line 157
  20. theorem OAI.Erdos3.FixedDensity.simplexCoordinatesOfAP_one line 164
  21. theorem OAI.Erdos3.FixedDensity.simplexCoordinatesOfAP_succ_succ line 171
  22. theorem OAI.Erdos3.FixedDensity.simplexCoordinateSum_decompose line 176
  23. theorem OAI.Erdos3.FixedDensity.simplexCoordinateMoment_decompose line 184
  24. theorem OAI.Erdos3.FixedDensity.simplexCoordinateSum_coordinatesOfAP line 192
  25. theorem OAI.Erdos3.FixedDensity.simplexCoordinateMoment_coordinatesOfAP line 201
  26. def OAI.Erdos3.FixedDensity.simplexAPEquiv line 208
  27. theorem OAI.Erdos3.FixedDensity.mean_equiv line 257
  28. theorem OAI.Erdos3.FixedDensity.mean_prod line 263
  29. theorem OAI.Erdos3.FixedDensity.mean_prod_fst line 270
  30. theorem OAI.Erdos3.FixedDensity.apSimplexSystem_simplexCount_eq_cyclicAPCount line 280
  31. structure OAI.Erdos3.FixedDensity.SimplexHypergraph line 323
  32. def OAI.Erdos3.FixedDensity.SimplexHypergraph.edgeFinset line 328
  33. theorem OAI.Erdos3.FixedDensity.SimplexHypergraph.mem_edgeFinset line 336
  34. def OAI.Erdos3.FixedDensity.SimplexHypergraph.simplexFinset line 344
  35. theorem OAI.Erdos3.FixedDensity.SimplexHypergraph.mem_simplexFinset line 352
  36. def OAI.Erdos3.FixedDensity.SimplexHypergraph.toWeighted line 360
  37. theorem OAI.Erdos3.FixedDensity.SimplexHypergraph.toWeighted_edgeWeight_of_edge line 367
  38. theorem OAI.Erdos3.FixedDensity.SimplexHypergraph.toWeighted_edgeWeight_of_not_edge line 376
  39. theorem OAI.Erdos3.FixedDensity.SimplexHypergraph.toWeighted_edgeWeight_nonneg line 384
  40. theorem OAI.Erdos3.FixedDensity.SimplexHypergraph.toWeighted_edgeWeight_le_one line 392
  41. theorem OAI.Erdos3.FixedDensity.SimplexHypergraph.toWeighted_simplexWeight_eq_indicator line 400
  42. theorem OAI.Erdos3.FixedDensity.SimplexHypergraph.toWeighted_simplexCount_eq_card_div line 426
  43. def OAI.Erdos3.FixedDensity.SimplexHypergraph.IsSimplexCover line 441
  44. theorem OAI.Erdos3.FixedDensity.SimplexHypergraph.isSimplexCover_iff line 448
  45. theorem OAI.Erdos3.FixedDensity.prod_sub_prod_eq_sum_ordered line 482
  46. def OAI.Erdos3.FixedDensity.mixedSimplexTerm line 509
  47. theorem OAI.Erdos3.FixedDensity.simplexWeight_sub_eq_sum_mixed line 519
  48. def OAI.Erdos3.FixedDensity.mixedSimplexCorrelation line 538
  49. theorem OAI.Erdos3.FixedDensity.simplexCount_sub_eq_sum_mixedCorrelation line 544
  50. theorem OAI.Erdos3.FixedDensity.abs_simplexCount_sub_le_sum_mixedCorrelation line 565
  51. def OAI.Erdos3.FixedDensity.MixedSimplexCorrelationLe line 574
  52. theorem OAI.Erdos3.FixedDensity.simplexCount_abs_sub_le_of_mixedCorrelation line 580