OAI/Probability/Subsphere/Estimates/FixedPrecision.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SubsphereCurrent.Fixed.boundConstant line 12
2. lemma OAI.SubsphereCurrent.Fixed.boundConstant_pos line 13
3. lemma OAI.SubsphereCurrent.Fixed.two_le_boundConstant line 14
4. lemma OAI.SubsphereCurrent.Fixed.parameters line 19
5. lemma OAI.SubsphereCurrent.Fixed.raw_bound_le line 38
6. lemma OAI.SubsphereCurrent.Fixed.dimension_bound_one_seed line 106
7. theorem OAI.SubsphereCurrent.Fixed.dimension_estimate line 155