OAI/Analysis/BernoulliCone/SmallPerturbation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Bernoulli.Shape.perturbation_lower line 15
2. lemma OAI.Bernoulli.Shape.perturbation_bijective line 24
3. def OAI.Bernoulli.Shape.perturbationHomeomorph line 46

   Source documentation

   A small globally Lipschitz perturbation of the identity is an actual bi-Lipschitz homeomorphism, obtained by the contraction theorem.

   def perturbationHomeomorph {K : ℝ≥0} {f : E → E} (hf : LipschitzWith K f)
       (hK : K < 1) : E ≃ₜ E := by
   …

4. lemma OAI.Bernoulli.Shape.perturbationHomeomorph_apply line 62
5. lemma OAI.Bernoulli.Shape.perturbationHomeomorph_symm_lipschitz line 65
6. lemma OAI.Bernoulli.Shape.perturbationHomeomorph_symm_fixed line 80