OAI/Combinatorics/Chromatic/Histories/LocalHistoryFormula.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.ElementaryPositivity.QuantumTorus.LocalHistoryFormula line 14
2. def OAI.ElementaryPositivity.QuantumTorus.LocalHistoryFormula.eval line 23
3. def OAI.ElementaryPositivity.QuantumTorus.LocalHistoryFormula.Positive line 29
4. def OAI.ElementaryPositivity.QuantumTorus.LocalHistoryFormula.Bounded line 35
5. def OAI.ElementaryPositivity.QuantumTorus.LocalHistoryFormula.sumList line 41
6. lemma OAI.ElementaryPositivity.QuantumTorus.LocalHistoryFormula.eval_sumList line 45
7. lemma OAI.ElementaryPositivity.QuantumTorus.LocalHistoryFormula.positive_sumList line 50
8. lemma OAI.ElementaryPositivity.QuantumTorus.LocalHistoryFormula.bounded_sumList line 55
9. lemma OAI.ElementaryPositivity.QuantumTorus.LocalHistoryFormula.eval_positive line 60
10. def OAI.ElementaryPositivity.QuantumTorus.LocalHistoryFormula.finSum line 83
11. lemma OAI.ElementaryPositivity.QuantumTorus.LocalHistoryFormula.eval_finSum line 85
12. lemma OAI.ElementaryPositivity.QuantumTorus.LocalHistoryFormula.positive_finSum line 90
13. lemma OAI.ElementaryPositivity.QuantumTorus.LocalHistoryFormula.bounded_finSum line 96
14. lemma OAI.ElementaryPositivity.QuantumTorus.common_history_producer line 111