OAI/Analysis/StrictMeans/DerivativeDistortion.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.StrictInverseFirstPower.second_deriv_normalize line 16
  2. theorem OAI.StrictInverseFirstPower.preSchwarzian_bound line 24
  3. lemma OAI.StrictInverseFirstPower.hasDerivAt_log_norm line 75
  4. lemma OAI.StrictInverseFirstPower.radial_preSchwarzian_bounds line 96
  5. lemma OAI.StrictInverseFirstPower.hasDerivAt_radial_log_deriv line 135
  6. lemma OAI.StrictInverseFirstPower.log_derivative_distortion_radial line 145
  7. theorem OAI.StrictInverseFirstPower.derivative_distortion line 213