OAI/Geometry/NearbyLagrangian/Radialization.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Degree-two radial extensions and their value and derivative estimates.

  1. theorem OAI.NearbyLagrangian.MixedRadial.hasFDerivAt_zero_of_quadratic_bound line 16
  2. theorem OAI.NearbyLagrangian.MixedRadial.exists_quadratic_bound line 32
  3. theorem OAI.NearbyLagrangian.MixedRadial.differentiable_degree_two line 59
  4. theorem OAI.NearbyLagrangian.MixedRadial.fderiv_smul_degree_two line 70
  5. theorem OAI.NearbyLagrangian.MixedRadial.exists_uniform_derivative_bound line 88
  6. lemma OAI.NearbyLagrangian.AngularExtension.contDiff_one_degree_two line 131
  7. def OAI.NearbyLagrangian.AngularExtension.radialize line 169
  8. lemma OAI.NearbyLagrangian.AngularExtension.radialize_zero line 171
  9. lemma OAI.NearbyLagrangian.AngularExtension.radialize_homogeneous line 173
  10. lemma OAI.NearbyLagrangian.AngularExtension.radialize_on_unit line 179
  11. lemma OAI.NearbyLagrangian.AngularExtension.contDiffAt_normalize line 182
  12. lemma OAI.NearbyLagrangian.AngularExtension.contDiffAt_radialize line 186
  13. lemma OAI.NearbyLagrangian.AngularExtension.contDiff_one_radialize line 191
  14. lemma OAI.NearbyLagrangian.AngularExtension.hasFDerivAt_normalize_unit line 206
  15. lemma OAI.NearbyLagrangian.AngularExtension.norm_fderiv_normalize_unit_le line 221
  16. lemma OAI.NearbyLagrangian.AngularExtension.fderiv_radialize_unit line 239
  17. lemma OAI.NearbyLagrangian.AngularExtension.radialize_eq_of_degree_two line 256
  18. lemma OAI.NearbyLagrangian.AngularExtension.norm_fderiv_radialize_sub_le line 265