OAI/Computability/DepthThree/UniformSparseBounds.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DepthThreeLowerBound.sparseEnvelope line 16
2. theorem OAI.DepthThreeLowerBound.sparse_expression_le_envelope line 21
3. theorem OAI.DepthThreeLowerBound.tendsto_sparseEnvelope line 82
4. theorem OAI.DepthThreeLowerBound.uniform_sparse_condition line 107
5. theorem OAI.DepthThreeLowerBound.hard_slice_tail_bounds line 124
6. theorem OAI.DepthThreeLowerBound.in_window_correlation_bound line 137