OAI/NumberTheory/Ostmann/QuadraticCenter/QuadraticAtom.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.QuadraticCenter.quadraticAtom line 8
2. theorem OAI.Ostmann.QuadraticCenter.inv_sqrt_scale_nonneg_le_one line 11
3. theorem OAI.Ostmann.QuadraticCenter.norm_quadraticAtom line 16
4. theorem OAI.Ostmann.QuadraticCenter.phase_quadratic_parameter_bound line 27
5. theorem OAI.Ostmann.QuadraticCenter.quadraticAtom_theta_lipschitz line 35
6. theorem OAI.Ostmann.QuadraticCenter.quadraticAtom_scale_lipschitz line 53
7. theorem OAI.Ostmann.QuadraticCenter.quadraticAtom_parameters_lipschitz line 84