OAI/Geometry/ProjectionBodies/Brouwer.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PettyProjection.FixedPoint.contDiffAt_rayRetraction line 13
2. lemma OAI.PettyProjection.FixedPoint.smooth_fixedPoint_ball line 29
3. lemma OAI.PettyProjection.FixedPoint.scaled_approximation line 59
4. lemma OAI.PettyProjection.FixedPoint.uniformlyContinuous_ball_extension line 91
5. lemma OAI.PettyProjection.FixedPoint.fixedPoint_unitBall line 111

   Source documentation

   The full continuous finite-dimensional unit-ball fixed-point theorem, obtained from polynomial Jacobian integration, not from a topological axiom.

   lemma fixedPoint_unitBall {f : E → E} (hf : ContinuousOn f (closedBall (0:E) 1))
       (hball : MapsTo f (closedBall (0:E) 1) (closedBall (0:E) 1)) :
       ∃ x∈closedBall (0:E) 1, f x=x := by
   …

6. theorem OAI.PettyProjection.FixedPoint.fixedPoint_compact_convex line 155

   Source documentation

   Brouwer on any nonempty compact convex set, derived from the genuine unit-ball theorem by the nearest-point extension.

   theorem fixedPoint_compact_convex {K : Set E} (hne : K.Nonempty)
       (hk : IsCompact K) (hc : Convex ℝ K) {f : E → E}
       (hf : ContinuousOn f K) (hmap : MapsTo f K K) : ∃ x∈K, f x=x := by
   …