OAI/Combinatorics/Progressions/FixedDensity/OrderedPattern.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Erdos3.FixedDensity.OrderedFace line 11
  2. instance OAI.Erdos3.FixedDensity.orderedFaceDecidableEq line 14
  3. def OAI.Erdos3.FixedDensity.orderedFaceTuple line 20
  4. abbrev OAI.Erdos3.FixedDensity.OrderedFaceComplement line 26
  5. def OAI.Erdos3.FixedDensity.orderedFaceSumEquiv line 30
  6. def OAI.Erdos3.FixedDensity.splitOrderedFaceEquiv line 38
  7. theorem OAI.Erdos3.FixedDensity.splitOrderedFaceEquiv_fst line 48
  8. def OAI.Erdos3.FixedDensity.orderedFaceComplementTuple line 58
  9. theorem OAI.Erdos3.FixedDensity.splitOrderedFaceEquiv_snd line 65
  10. theorem OAI.Erdos3.FixedDensity.orderedFaceTuple_splitOrderedFaceEquiv_symm line 75
  11. theorem OAI.Erdos3.FixedDensity.orderedFaceComplementTuple_splitOrderedFaceEquiv_symm line 85
  12. theorem OAI.Erdos3.FixedDensity.mean_splitOrderedFace line 94
  13. theorem OAI.Erdos3.FixedDensity.exists_orderedFace_coordinate_not_mem_range line 118
  14. def OAI.Erdos3.FixedDensity.orderedFaceMissingCoordinate line 144
  15. theorem OAI.Erdos3.FixedDensity.orderedFaceMissingCoordinate_not_mem_range line 150
  16. structure OAI.Erdos3.FixedDensity.WeightedOrderedPattern line 157
  17. def OAI.Erdos3.FixedDensity.WeightedOrderedPattern.patternWeight line 163
  18. def OAI.Erdos3.FixedDensity.WeightedOrderedPattern.patternCount line 170
  19. def OAI.Erdos3.FixedDensity.WeightedOrderedPattern.EdgeWeightsInUnitInterval line 175
  20. theorem OAI.Erdos3.FixedDensity.WeightedOrderedPattern.patternWeight_nonneg line 180
  21. theorem OAI.Erdos3.FixedDensity.WeightedOrderedPattern.patternCount_nonneg line 188
  22. structure OAI.Erdos3.FixedDensity.OrderedPattern line 197
  23. def OAI.Erdos3.FixedDensity.OrderedPattern.IsOccurrence line 203
  24. def OAI.Erdos3.FixedDensity.OrderedPattern.occurrenceFinset line 209
  25. theorem OAI.Erdos3.FixedDensity.OrderedPattern.mem_occurrenceFinset line 217
  26. def OAI.Erdos3.FixedDensity.OrderedPattern.toWeighted line 224
  27. theorem OAI.Erdos3.FixedDensity.OrderedPattern.toWeighted_edgeWeight_nonneg line 233
  28. theorem OAI.Erdos3.FixedDensity.OrderedPattern.toWeighted_edgeWeight_le_one line 242
  29. theorem OAI.Erdos3.FixedDensity.OrderedPattern.toWeighted_unitInterval line 251
  30. theorem OAI.Erdos3.FixedDensity.OrderedPattern.toWeighted_patternWeight_of_occurrence line 259
  31. theorem OAI.Erdos3.FixedDensity.OrderedPattern.toWeighted_patternWeight_of_not_occurrence line 270
  32. theorem OAI.Erdos3.FixedDensity.OrderedPattern.toWeighted_patternCount_eq line 281
  33. abbrev OAI.Erdos3.FixedDensity.OrderedPattern.DeletionFamily line 303
  34. def OAI.Erdos3.FixedDensity.OrderedPattern.IsCover line 307
  35. def OAI.Erdos3.FixedDensity.OrderedPattern.faceDeletionDensity line 315
  36. def OAI.Erdos3.FixedDensity.OrderedPattern.emptyDeletion line 322
  37. theorem OAI.Erdos3.FixedDensity.OrderedPattern.faceDeletionDensity_empty line 328
  38. def OAI.Erdos3.FixedDensity.HasUniformOrderedPatternRemoval line 337
  39. theorem OAI.Erdos3.FixedDensity.OrderedPattern.isOccurrence_all_of_rank_zero line 348
  40. theorem OAI.Erdos3.FixedDensity.hasUniformOrderedPatternRemoval_zero line 363