OAI/Geometry/HeilbronnTriangle/FixedDetReduction.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem355.FixedDetReduction.radius line 12
2. lemma OAI.Problem355.FixedDetReduction.log_radius_bound line 14
3. lemma OAI.Problem355.FixedDetReduction.radius_antitone line 35
4. lemma OAI.Problem355.FixedDetReduction.one_le_radius line 40
5. lemma OAI.Problem355.FixedDetReduction.radius_product_bound line 46
6. theorem OAI.Problem355.FixedDetReduction.radius_count_factor_bound line 57
7. lemma OAI.Problem355.FixedDetReduction.coordinate_radius_le line 82
8. def OAI.Problem355.FixedDetReduction.AnisotropicEstimate line 100
9. theorem OAI.Problem355.FixedDetReduction.fixed_det_count_of_short_basis line 107