У меня есть один давно незакрытый гештальт по поводу оперирования со значками
и
, а тут как раз выдался подходящий момент и я решил таки разобраться со всем этим. В общем, дело в том, что я не очень умею пользоваться этими значками и, как я думаю, немало теряю из-за этого. Разумеется, я способен использовать что-то в духе
и подобные простые примеры, но мне этого мало. Вот буквально вчера я что-то доказывал, связанное с определителями, и я более менее мог писать выражения вида
Как я для себя обосновывал равенство, например, первой и третьей строчки. Я понимаю, что перестановки образуют группу
, в группе любое уравнение
или
разрешимо и при том единственным образом, поэтому для любого
(где
). Я знаю, что это так себе объяснение
, можете не говорить)) Хоть и формально корректное.
Но мне хочется оперировать суммами автоматически, не думая. Почему-то проблеме оперирования с суммами/произведениями уделяется довольно мало времени, несмотря на то, что эта тема довольно глубокая. Единственное место из мне известных, где что-то говорят о суммах - это вторая глава в "Конкретной математике". Но это слишком слабый уровень.
Мне хочется почитать общую теорию. Вот в том примере выше, например, использовался факт из теории групп. Да, можно его не использовать, а воспользоваться тем, что любая перестановка - это биекция, а значит все в порядке. Это еще один вариант обоснования. Но хочется пойти еще дальше (и думать еще меньше). Хочется использовать, например, машинерию из логики. Да, в "Конкретной математике" рассказывают про скобку Айверсона, но блин... это все такой незначительный уровень... Нужна теория для сумм со сложными логическими предикатами, чтобы там во всю использовались булевы функции, полиномы Жигалкина, конечные поля и так далее. Чтобы можно было суммировать по произвольной области индексации, чтобы можно было не думать, является ли функция смены индексации биекцией или нет (я думаю, это можно было бы достичь какой-нибудь нотацией, навешивающей на аргумент какой-нибудь алгебраический инвариант). Чтобы можно было комбинировать какими-нибудь нетривиальными способами области идексаций:
минимум по линии теоретико-множественных операций (а так-то хочется, например, использовать алгебраическую или иную структуру на множестве индексов и иметь нотацию, которая бы как-нибудь хитро все это дело миксовала, факторизовала и т.д). И чтобы это можно было делать автоматически, не думая.
Для всего этого нужен хороший корпус разработанных теорем и нотаций. Кажется, что это все не шибко уж сложные вещи и должно уже быть сделано. Хотелось бы узнать, встречал ли кто-нибудь такую "общую теорию сумм/произведений" и где об этом можно подробно и обстоятельно почитать (желательно на высоком уровне абстракции и с использованием аппаратов логики, алгебры и т.д.)