OAI/Combinatorics/SquareDifference/PairBridge.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SquareDifference.PairBridge.actualLiftPiece_eq line 22
2. lemma OAI.SquareDifference.PairBridge.actualSupportFamily_eq line 29
3. def OAI.SquareDifference.PairBridge.sequenceCoeff line 36
4. lemma OAI.SquareDifference.PairBridge.gateCoefficient_empty line 39
5. lemma OAI.SquareDifference.PairBridge.actualPiece_polynomial line 44
6. lemma OAI.SquareDifference.PairBridge.polynomial_sum line 55
7. lemma OAI.SquareDifference.PairBridge.actualLift_polynomial line 62
8. lemma OAI.SquareDifference.PairBridge.actualLift_fourier line 82
9. lemma OAI.SquareDifference.PairBridge.sequenceCoeff_bound line 87
10. lemma OAI.SquareDifference.PairBridge.actualLift_pointwise_bound line 108
11. lemma OAI.SquareDifference.PairBridge.actualLift_mean line 130
12. lemma OAI.SquareDifference.PairBridge.actualFamily_polynomial line 142
13. lemma OAI.SquareDifference.PairBridge.actualFamily_fourier line 162
14. lemma OAI.SquareDifference.PairBridge.frozenFamily_fourier line 167
15. lemma OAI.SquareDifference.PairBridge.frozen_lift_low_fourier line 179
16. def OAI.SquareDifference.PairBridge.gatedSequence line 195
17. lemma OAI.SquareDifference.PairBridge.frozen_low_lift_gated line 198
18. lemma OAI.SquareDifference.PairBridge.frozen_lift_fiber_fourier line 213