OAI/Geometry/PrescribedRicci/TameLocalInverse.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Tame Local Inverse.

  1. lemma OAI.SobolevChart.perturbation_commutator_bound line 22
  2. structure OAI.FrozenPoisson.ParameterRegularity.TameData line 58
  3. lemma OAI.FrozenPoisson.ParameterRegularity.tame_word_bound line 67
  4. lemma OAI.FrozenPoisson.ParameterRegularity.tame_preestimate line 114
  5. theorem OAI.FrozenPoisson.ParameterRegularity.tame_estimate line 125
  6. lemma OAI.FrozenPoisson.ParameterRegularity.combine_estimate line 151
  7. lemma OAI.FrozenPoisson.ParameterRegularity.tame_low_estimate line 156
  8. theorem OAI.FrozenPoisson.ParameterRegularity.tame_solution_bound line 177
  9. theorem OAI.FrozenPoisson.ParameterRegularity.tame_inverse_bound line 190