OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/HalfGeometricIdentity.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OrdinaryChainScales.half_geometric_identity line 25
2. lemma OAI.OrdinaryChainScales.half_geometric_le line 31
3. lemma OAI.OrdinaryChainScales.geometric_error_sum line 36
4. lemma OAI.OrdinaryChainScales.mesh_strict line 43
5. lemma OAI.OrdinaryChainScales.mesh_linear_growth line 50
6. lemma OAI.OrdinaryChainScales.exp_mesh_geometric line 55
7. lemma OAI.OrdinaryChainScales.mesh_zero_exp line 67
8. lemma OAI.OrdinaryChainScales.dyadic_cutoff_of_power line 82
9. lemma OAI.OrdinaryChainScales.all_previous_power_cutoffs line 88
10. lemma OAI.OrdinaryChainScales.all_good_energy line 97