OAI/Geometry/ProjectionBodies/FixedPointCalculus.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PettyProjection.FixedPoint.rayRoot line 11
  2. lemma OAI.PettyProjection.FixedPoint.rayRoot_positive line 12
  3. lemma OAI.PettyProjection.FixedPoint.rayRoot_quadratic line 19
  4. lemma OAI.PettyProjection.FixedPoint.rayRoot_eq_one line 27
  5. def OAI.PettyProjection.FixedPoint.rayRetraction line 37
  6. lemma OAI.PettyProjection.FixedPoint.norm_add_smul_sq line 40
  7. lemma OAI.PettyProjection.FixedPoint.rayRetraction_norm line 47
  8. lemma OAI.PettyProjection.FixedPoint.rayRetraction_boundary line 56
  9. def OAI.PettyProjection.FixedPoint.ContinuousCoeffs line 75
  10. lemma OAI.PettyProjection.FixedPoint.continuousCoeffs_const line 78
  11. lemma OAI.PettyProjection.FixedPoint.continuousCoeffs_C line 81
  12. lemma OAI.PettyProjection.FixedPoint.ContinuousCoeffs.add line 88
  13. lemma OAI.PettyProjection.FixedPoint.ContinuousCoeffs.mul line 95
  14. lemma OAI.PettyProjection.FixedPoint.ContinuousCoeffs.sum line 102
  15. lemma OAI.PettyProjection.FixedPoint.ContinuousCoeffs.prod line 109
  16. lemma OAI.PettyProjection.FixedPoint.ContinuousCoeffs.det line 120
  17. def OAI.PettyProjection.FixedPoint.integralPolynomial line 134

    Source documentation

    Integrating a uniformly bounded-degree polynomial coefficient by coefficient.

    def integralPolynomial {α : Type uα} [MeasurableSpace α] (μ : Measure α)
    (p : α → Polynomial ℝ) (d : ℕ) : Polynomial ℝ :=
…
  18. lemma OAI.PettyProjection.FixedPoint.eval_integralPolynomial line 138
  19. lemma OAI.PettyProjection.FixedPoint.exists_integral_det_polynomial line 153
  20. lemma OAI.PettyProjection.FixedPoint.exists_integralOn_det_polynomial line 181
  21. lemma OAI.PettyProjection.FixedPoint.exists_integralOn_clm_det_polynomial line 213
  22. lemma OAI.PettyProjection.FixedPoint.bijective_add_small line 241
  23. lemma OAI.PettyProjection.FixedPoint.image_ball_add_small line 267
  24. lemma OAI.PettyProjection.FixedPoint.image_closedBall_add_small line 287
  25. lemma OAI.PettyProjection.FixedPoint.nearest_unique line 317
  26. def OAI.PettyProjection.FixedPoint.nearest line 331

    Source documentation

    The genuine nearest point; no fixed-point principle is used here.

    def nearest (K : Set E) (hne : K.Nonempty) (hcomplete : IsComplete K)
    (hc : Convex ℝ K) (x : E) : E :=
…
  27. lemma OAI.PettyProjection.FixedPoint.nearest_mem line 335
  28. lemma OAI.PettyProjection.FixedPoint.nearest_inner line 339
  29. lemma OAI.PettyProjection.FixedPoint.nearest_eq_of_mem line 345
  30. lemma OAI.PettyProjection.FixedPoint.nearest_eq_of_inner line 352
  31. lemma OAI.PettyProjection.FixedPoint.nearest_lipschitz line 358
  32. def OAI.PettyProjection.FixedPoint.ballNearest line 383
  33. lemma OAI.PettyProjection.FixedPoint.ballNearest_mem line 386
  34. lemma OAI.PettyProjection.FixedPoint.ballNearest_eq line 389
  35. lemma OAI.PettyProjection.FixedPoint.ballNearest_lipschitz line 392
  36. lemma OAI.PettyProjection.FixedPoint.ballNearest_norm line 396
  37. lemma OAI.PettyProjection.FixedPoint.ball_uniqueDiff line 424
  38. lemma OAI.PettyProjection.FixedPoint.sphere_derivative_det_zero line 429
  39. lemma OAI.PettyProjection.FixedPoint.retraction_extension line 458
  40. lemma OAI.PettyProjection.FixedPoint.eventually_pos_det_homotopy line 500
  41. lemma OAI.PettyProjection.FixedPoint.no_smooth_retraction line 525

    Source documentation

    Milnor's elementary determinant-polynomial obstruction to a differentiable retraction of a ball onto its sphere. Only Jacobian change of variables and the Banach contraction principle are needed.

    lemma no_smooth_retraction (μ : Measure E) [μ.IsAddHaarMeasure]
    {r : E → E} {r' : E → E →L[ℝ] E}
    (hd : ∀ x∈closedBall (0:E) 1, HasFDerivWithinAt r (r' x) (closedBall (0:E) 1) x)
    (hc : ContinuousOn r' (closedBall (0:E) 1))
    (hnorm : ∀ x∈closedBall (0:E) 1, ‖r x‖=1)
    (hb : ∀ x : E, ‖x‖=1 → r x=x) : False := by
…