OAI/Combinatorics/Progressions/Estimates/NativeBinaryAssignments.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.firstTranslationCoordinate line 14
  2. def OAI.Erdos3.translationExpansionRemainder line 18
  3. theorem OAI.Erdos3.coordinateTranslationExpansion_factor line 24
  4. theorem OAI.Erdos3.coordinateTranslationExpansion_norm_le_one line 37
  5. theorem OAI.Erdos3.translationExpansionRemainder_norm_le_one line 47
  6. def OAI.Erdos3.ternaryIndexOfFunction line 68
  7. def OAI.Erdos3.ternaryLeafInput line 74
  8. theorem OAI.Erdos3.ternaryReplaceInput_zero line 79
  9. theorem OAI.Erdos3.prod_fin_succ_function line 87
  10. theorem OAI.Erdos3.ternaryCoordinateExpansion_leaves line 94
  11. def OAI.Erdos3.binaryIndexOfFunction line 120
  12. def OAI.Erdos3.binaryLeafInput line 125
  13. theorem OAI.Erdos3.coordinateTranslationExpansion_leaves line 131
  14. def OAI.Erdos3.finiteChoiceCoordinateInput line 160
  15. def OAI.Erdos3.finiteChoiceCoordinateHom line 163
  16. def OAI.Erdos3.finiteChoiceReplaceIndex line 170
  17. def OAI.Erdos3.finiteChoiceReplaceInput line 173
  18. theorem OAI.Erdos3.finiteChoiceCoordinateInput_replace line 177
  19. theorem OAI.Erdos3.finiteChoiceCoordinateInput_cons line 187
  20. def OAI.Erdos3.finiteChoiceLeafInput line 197
  21. def OAI.Erdos3.finiteChoiceExpansion line 202
  22. theorem OAI.Erdos3.finiteChoiceExpansion_cons line 206
  23. theorem OAI.Erdos3.finiteChoiceExpansion_unit line 213
  24. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_translation_expansion_equivalence line 232
  25. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_finite_assignment_equivalence line 300
  26. def OAI.Erdos3.mixedTranslationCoordinates line 417
  27. theorem OAI.Erdos3.mem_mixedTranslationCoordinates line 421
  28. theorem OAI.Erdos3.mixedTranslationCoordinates_nodup line 425
  29. def OAI.Erdos3.mixedTranslationSample line 428
  30. def OAI.Erdos3.mixedTranslationSampleHom line 433
  31. theorem OAI.Erdos3.mixedTranslationSample_translated line 445
  32. theorem OAI.Erdos3.replicatedMixed_nonempty line 452
  33. theorem OAI.Erdos3.replicatedMixed_card line 455
  34. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedTranslationExpansion_factor line 463
  35. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_mixed_translation_equivalence line 472
  36. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_binary_assignment_equivalence line 504