OAI/Analysis/IntegralMeans/CriticalPoint.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Brennan.second_derivative_nonneg_at_min_zero line 21
  2. lemma OAI.Brennan.second_directional_nonneg_at_min line 52
  3. lemma OAI.Brennan.differentiableAt_fderiv_logPotential_apply line 72
  4. lemma OAI.Brennan.not_isLocalMin_logPotential line 95
  5. def OAI.Brennan.reciprocalPotential line 115
  6. lemma OAI.Brennan.continuousOn_reciprocalPotential line 118
  7. lemma OAI.Brennan.reciprocalPotential_pos line 125
  8. lemma OAI.Brennan.log_reciprocalPotential line 129
  9. lemma OAI.Brennan.not_isLocalMax_reciprocalPotential line 136
  10. lemma OAI.Brennan.reciprocalPotential_lt_boundary line 148
  11. def OAI.Brennan.regularizedGradient line 182
  12. lemma OAI.Brennan.regularizedGradient_eq_zero_iff line 185
  13. lemma OAI.Brennan.differentiableAt_gradientCoefficient line 193
  14. lemma OAI.Brennan.differentiableAt_regularizedGradient line 201
  15. lemma OAI.Brennan.hasFDerivAt_regularizedGradient_at_critical line 208
  16. lemma OAI.Brennan.hasFDerivAt_regularizedGradient_at_pole line 220
  17. lemma OAI.Brennan.det_conj_comp line 232
  18. lemma OAI.Brennan.det_regularizedGradient_at_critical line 240
  19. lemma OAI.Brennan.det_regularizedGradient_at_pole_pos line 251