OAI/Combinatorics/SumProduct/Alignment/AllLevel15.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AllLevelFactorization.Factorization.ResidueCover.pointEvaluation_levels line 31
2. theorem OAI.AllLevelFactorization.Factorization.ResidueCover.physical_faces_of_marginal_haar line 51
3. def OAI.AllLevelFactorization.Factorization.ResidueCover.physicalData_of_haar line 121
4. def OAI.RationalLattice.PolynomialArrays.shiftAction line 158
5. lemma OAI.RationalLattice.PolynomialArrays.shiftAction_continuous line 169
6. lemma OAI.RationalLattice.PolynomialArrays.shiftAction_mk line 174
7. lemma OAI.RationalLattice.PolynomialArrays.readout_shiftAction line 179
8. theorem OAI.AllLevelFactorization.Factorization.empirical_success_from_marginal_haar line 258