OAI/NumberTheory/PiExponent/Ampleness/AdmissibleBlowupPolarization.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PiExponent.AdmissibleBlowupGeometry.exists_ampleExponent line 12
2. def OAI.PiExponent.AdmissibleBlowupGeometry.ampleExponent line 16
3. theorem OAI.PiExponent.AdmissibleBlowupGeometry.ampleExponent_gt_one line 18
4. def OAI.PiExponent.AdmissibleBlowupGeometry.H line 20
5. theorem OAI.PiExponent.AdmissibleBlowupGeometry.H_ample line 22
6. def OAI.PiExponent.AdmissibleBlowupGeometry.interpolationBundle line 24
7. def OAI.PiExponent.AdmissibleBlowupGeometry.uniformMargin line 26
8. theorem OAI.PiExponent.AdmissibleBlowupGeometry.uniformMargin_pos line 28
9. theorem OAI.PiExponent.AdmissibleBlowupGeometry.uniform_curve_margin_of_affine_curve_data line 31