OAI/Analysis/IntegralMeans/CriticalMap.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Brennan.logarithmicJet line 21
  2. lemma OAI.Brennan.logarithmicJet_eq line 24
  3. def OAI.Brennan.criticalMap line 34
  4. def OAI.Brennan.normalizedJacobian line 37
  5. lemma OAI.Brennan.fderiv_criticalMap_apply line 40
  6. lemma OAI.Brennan.criticalMap_columns line 62
  7. lemma OAI.Brennan.critical_columns_det line 73
  8. lemma OAI.Brennan.normalizedJacobian_formula line 83
  9. lemma OAI.Brennan.hasDerivAt_reciprocalDeriv line 99
  10. lemma OAI.Brennan.logarithmicJet_reroot line 106
  11. lemma OAI.Brennan.criticalMap_reroot line 124
  12. lemma OAI.Brennan.normalizedJacobian_reroot line 137
  13. def OAI.Brennan.potential line 144
  14. def OAI.Brennan.GoodPair line 147
  15. def OAI.Brennan.CriticalCountStatement line 151
  16. lemma OAI.Brennan.differentiableAt_criticalMap line 160
  17. lemma OAI.Brennan.critical_fiber_discrete line 168
  18. lemma OAI.Brennan.finite_critical_superlevel line 188
  19. def OAI.Brennan.logPotential line 208
  20. lemma OAI.Brennan.differentiableAt_log_norm line 211
  21. lemma OAI.Brennan.fderiv_log_norm_apply line 216
  22. lemma OAI.Brennan.differentiableAt_logPotential line 234
  23. lemma OAI.Brennan.fderiv_logPotential_apply line 241
  24. lemma OAI.Brennan.criticalMap_ne_pole line 256
  25. lemma OAI.Brennan.critical_difference line 266
  26. lemma OAI.Brennan.ratio_at_critical line 272
  27. lemma OAI.Brennan.criticalMap_eq_of_ratio line 282
  28. lemma OAI.Brennan.critical_iff_fderiv_logPotential_zero line 294
  29. def OAI.Brennan.targetRatio line 323
  30. lemma OAI.Brennan.hasDerivAt_targetRatio line 325
  31. lemma OAI.Brennan.deriv_targetRatio_at_critical line 333
  32. def OAI.Brennan.secondDirectional line 346
  33. def OAI.Brennan.realHessian line 349
  34. lemma OAI.Brennan.secondDirectional_logPotential_one line 353
  35. lemma OAI.Brennan.secondDirectional_logPotential_I line 373
  36. lemma OAI.Brennan.realHessian_logPotential line 399
  37. lemma OAI.Brennan.trace_realHessian_logPotential line 408
  38. lemma OAI.Brennan.realHessian_at_critical line 414
  39. lemma OAI.Brennan.det_realHessian_at_critical line 439
  40. lemma OAI.Brennan.trace_realHessian_negative line 453
  41. lemma OAI.Brennan.det_realHessian_ne_zero_at_critical line 459
  42. lemma OAI.Brennan.potential_off_pole line 468
  43. lemma OAI.Brennan.potential_pos line 474
  44. lemma OAI.Brennan.potential_at_pole line 480
  45. lemma OAI.Brennan.potential_critical_height line 486
  46. lemma OAI.Brennan.critical_target_weight line 500