OAI/Analysis/StrictMeans/HessianLocal.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.StrictInverseFirstPower.Grid.complex_real_decomposition line 11
  2. lemma OAI.StrictInverseFirstPower.Grid.realCLM_apply line 14
  3. lemma OAI.StrictInverseFirstPower.Grid.realCLM_eq_zero line 19
  4. def OAI.StrictInverseFirstPower.Grid.planeCLM line 23
  5. lemma OAI.StrictInverseFirstPower.Grid.planeCLM_apply line 25
  6. def OAI.StrictInverseFirstPower.Grid.hessianCLM line 28
  7. lemma OAI.StrictInverseFirstPower.Grid.hessianCLM_apply line 31
  8. lemma OAI.StrictInverseFirstPower.Grid.hessianCLM_injective line 36
  9. lemma OAI.StrictInverseFirstPower.Grid.injectiveCLM_lower_bound line 49
  10. lemma OAI.StrictInverseFirstPower.Grid.hessianCLM_of_second line 59
  11. lemma OAI.StrictInverseFirstPower.Grid.quadratic_contDiff line 77
  12. lemma OAI.StrictInverseFirstPower.Grid.quadratic_fderiv line 83
  13. def OAI.StrictInverseFirstPower.Grid.affinePotential line 101
  14. lemma OAI.StrictInverseFirstPower.Grid.affinePotential_contDiffAt line 103
  15. lemma OAI.StrictInverseFirstPower.Grid.affinePotential_spatial line 109
  16. lemma OAI.StrictInverseFirstPower.Grid.local_quadratic_homotopy_regular line 122