OAI/Probability/Subsphere/Estimates/AffinePrecision.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SubsphereCurrent.Affine.log_two_bounds line 11
2. lemma OAI.SubsphereCurrent.Affine.log_thousand_lower line 19
3. lemma OAI.SubsphereCurrent.Affine.affine_parameters line 25
4. lemma OAI.SubsphereCurrent.Affine.log_card_of_width line 36
5. lemma OAI.SubsphereCurrent.Affine.affine_raw_bound line 50
6. lemma OAI.SubsphereCurrent.Affine.affine_zero_bound line 126
7. lemma OAI.SubsphereCurrent.Affine.simulated_numeric_bound line 154
8. lemma OAI.SubsphereCurrent.Affine.estimate_one_seed line 202
9. theorem OAI.SubsphereCurrent.Affine.all_affine_estimate line 227
10. theorem OAI.SubsphereCurrent.Affine.all_affine_full_estimate line 263