OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/ErrorSampleConstant.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OrdinaryChainScales.errorSampleConstant line 26
2. lemma OAI.OrdinaryChainScales.errorSampleConstant_nonneg line 29
3. lemma OAI.OrdinaryChainScales.sampled_stage_error_normalized line 33
4. lemma OAI.OrdinaryChainScales.prime_window_square_sum line 55
5. lemma OAI.OrdinaryChainScales.chain_mesh_large line 66
6. lemma OAI.OrdinaryChainScales.chain_window_error_width line 73
7. lemma OAI.OrdinaryChainScales.actual_error_width line 83
8. lemma OAI.OrdinaryChainScales.rational_error_budget line 95