OAI/Computability/DepthThree/InterpolationSigns.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DepthThreeLowerBound.Interpolation.bitEval line 20
2. theorem OAI.DepthThreeLowerBound.Interpolation.bitEval_apply line 30
3. theorem OAI.DepthThreeLowerBound.Interpolation.functional_surjective line 34
4. theorem OAI.DepthThreeLowerBound.Interpolation.bitEval_surjective line 40
5. def OAI.DepthThreeLowerBound.Interpolation.coefficientBits line 51
6. def OAI.DepthThreeLowerBound.Interpolation.acceptEval line 55
7. theorem OAI.DepthThreeLowerBound.Interpolation.acceptEval_eq_true line 59
8. def OAI.DepthThreeLowerBound.Interpolation.complementEquiv line 65
9. theorem OAI.DepthThreeLowerBound.Interpolation.finiteAvg_bitEval line 80
10. theorem OAI.DepthThreeLowerBound.Interpolation.finiteAvg_coefficientBits line 86
11. theorem OAI.DepthThreeLowerBound.Interpolation.finiteAvg_acceptEval line 96
12. theorem OAI.DepthThreeLowerBound.Interpolation.card_bitEval_fiber_mul line 117
13. theorem OAI.DepthThreeLowerBound.Interpolation.card_bitEval_fiber line 127
14. theorem OAI.DepthThreeLowerBound.Interpolation.finiteAvg_acceptEval_finset line 147