Contraction certificates

This file gives the small fixed-point argument used by a Krawczyk certificate. A contraction which preserves a complete nonempty set has a unique fixed point there. If the contraction is a preconditioned Newton map, that fixed point is the unique zero in the set.

theorem LeanPool.Besicovitch.existsUnique_fixedPoint_mem {E : Type u_1} [MetricSpace E] {K : NNReal} {T : E → E} {box : Set E} (hbox : box.Nonempty) (hcomplete : IsComplete box) (hmaps : Set.MapsTo T box box) (hcontract : ContractingWith K (Set.MapsTo.restrict T box box hmaps)) : ∃! x : E, x ∈ box ∧ Function.IsFixedPt T x

A contraction preserving a complete nonempty set has exactly one fixed point in that set.

theorem LeanPool.Besicovitch.existsUnique_zero_of_contracting_preconditioner {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {K : NNReal} {F T : E → E} {R : E →ₗ[ℝ] E} {box : Set E} (hbox : box.Nonempty) (hcomplete : IsComplete box) (hmaps : Set.MapsTo T box box) (hcontract : ContractingWith K (Set.MapsTo.restrict T box box hmaps)) (hupdate : ∀ x ∈ box, T x = x - R (F x)) (hR : Function.Injective ⇑R) : ∃! x : E, x ∈ box ∧ F x = 0

A certified preconditioned contraction isolates a unique zero of F in box.