theorem NewtonKantorovich.ContractingWith.eq_of_fixedPoints {α : Type u_1} [MetricSpace α] {K : NNReal} {f : α → α} {s : Set α} (hsf : Set.MapsTo f s s) (hf : ContractingWith K (Set.MapsTo.restrict f s s hsf)) {x y : α} (hxs : x ∈ s) (hys : y ∈ s) (hx : Function.IsFixedPt f x) (hy : Function.IsFixedPt f y) : x = y

A map that contracts on a forward-invariant set has at most one fixed point in that set.

noncomputable def NewtonKantorovich.ContractingWith.fixedPoint' {α : Type u_1} [MetricSpace α] [CompleteSpace α] {K : NNReal} (f : α → α) {s : Set α} (hsc : IsClosed s) (hs' : s.Nonempty) (hsf : Set.MapsTo f s s) (hf : ContractingWith K (Set.MapsTo.restrict f s s hsf)) : α

Let s be a complete, nonempty, forward-invariant set of a self-map f. If f contracts on s, then fixedPoint' is the unique fixed point of the restriction of f to s.

Equations

• NewtonKantorovich.ContractingWith.fixedPoint' f hsc hs' hsf hf = ContractingWith.efixedPoint' f ⋯ hsf hf (Exists.choose hs') ⋯ ⋯

theorem NewtonKantorovich.ContractingWith.fixedPoint'_mem {α : Type u_1} [MetricSpace α] [CompleteSpace α] {K : NNReal} {f : α → α} {s : Set α} (hsc : IsClosed s) (hs' : s.Nonempty) (hsf : Set.MapsTo f s s) (hf : ContractingWith K (Set.MapsTo.restrict f s s hsf)) : fixedPoint' f hsc hs' hsf hf ∈ s

The constructed fixed point lies in the invariant set.

theorem NewtonKantorovich.ContractingWith.fixedPoint'_isFixedPt {α : Type u_1} [MetricSpace α] [CompleteSpace α] {K : NNReal} {f : α → α} {s : Set α} (hsc : IsClosed s) (hs' : s.Nonempty) (hsf : Set.MapsTo f s s) (hf : ContractingWith K (Set.MapsTo.restrict f s s hsf)) : Function.IsFixedPt f (fixedPoint' f hsc hs' hsf hf)

The constructed point is genuinely fixed by f.

theorem NewtonKantorovich.ContractingWith.fixedPoint'_unique {α : Type u_1} [MetricSpace α] [CompleteSpace α] {K : NNReal} {f : α → α} {s : Set α} (hsc : IsClosed s) (hs' : s.Nonempty) (hsf : Set.MapsTo f s s) (hf : ContractingWith K (Set.MapsTo.restrict f s s hsf)) {x : α} (hxs : x ∈ s) (hx : Function.IsFixedPt f x) : x = fixedPoint' f hsc hs' hsf hf

Any fixed point of f in the invariant set is the constructed one.

theorem NewtonKantorovich.mem_closedBall_iff_nnnorm {E : Type u_4} [SeminormedAddCommGroup E] {a b : E} {r : NNReal} : b ∈ Metric.closedBall a ↑r ↔ ‖b - a‖₊ ≤ r

Membership in a closed ball, phrased with nnnorm.

theorem NewtonKantorovich.contractingWith_of_nnnorm_fderiv_le {X : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] {T : X → X} {DT : X → X →L[ℝ] X} (hT : ∀ (x : X), HasFDerivAt T (DT x) x) {x₀ : X} {r : NNReal} (hTx₀ : Set.MapsTo T (Metric.closedBall x₀ ↑r) (Metric.closedBall x₀ ↑r)) {K : NNReal} (hzK : K < 1) (hDT : ∀ {x : X}, x ∈ Metric.closedBall x₀ ↑r → ‖DT x‖₊ ≤ K) : ContractingWith K (Set.MapsTo.restrict T (Metric.closedBall x₀ ↑r) (Metric.closedBall x₀ ↑r) hTx₀)

Derivative criterion for ContractingWith.

theorem NewtonKantorovich.image_bound {X : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {T : X → X} {DT : X → X →L[ℝ] X} (hT : ∀ (x : X), HasFDerivAt T (DT x) x) (hDT : Continuous DT) {R : NNReal} {x₀ : X} {y z₁ z₂ : NNReal} (hy : ‖T x₀ - x₀‖₊ ≤ y) (hz₁ : ‖DT x₀‖₊ ≤ z₁) (hz₂ : ∀ x ∈ Metric.closedBall x₀ ↑R, ‖DT x - DT x₀‖₊ ≤ z₂ * ‖x - x₀‖₊) {r : NNReal} (hrR : r ≤ R) {x : X} (hx : x ∈ Metric.closedBall x₀ ↑r) : ‖T x - x₀‖₊ ≤ y + z₁ * r + z₂ * r ^ 2 / 2

Quantitative bound for the image of a point in a closed ball. This is the estimate that supplies the factor 1 / 2 in Newton--Kantorovich.

theorem NewtonKantorovich.contraction_mapping {X : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {T : X → X} {DT : X → X →L[ℝ] X} (hT : ∀ (x : X), HasFDerivAt T (DT x) x) (hDT : Continuous DT) {R : NNReal} {x₀ : X} {y z₁ z₂ : NNReal} (hy : ‖T x₀ - x₀‖₊ ≤ y) (hz₁ : ‖DT x₀‖₊ ≤ z₁) (hz₂ : ∀ x ∈ Metric.closedBall x₀ ↑R, ‖DT x - DT x₀‖₊ ≤ z₂ * ‖x - x₀‖₊) {r : NNReal} (hrR : r ≤ R) (hyr : y + z₁ * r + z₂ * r ^ 2 / 2 ≤ r) (hzr : z₁ + z₂ * r < 1) : ∃! x : X, T x = x ∧ ‖x - x₀‖₊ ≤ r

Quantitative contraction mapping theorem on a closed ball.

theorem NewtonKantorovich.newton_kantorovich {X : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {Y : Type u_3} [NormedAddCommGroup Y] [NormedSpace ℝ Y] {F : X → Y} {DF : X → X →L[ℝ] Y} (hF : ∀ (x : X), HasFDerivAt F (DF x) x) (hDF : Continuous DF) {A : Y →L[ℝ] X} (hA : Function.Injective ⇑A) {R : ENNReal} {x₀ : X} {y z₁ z₂ : NNReal} (hy : ‖A (F x₀)‖₊ ≤ y) (hz₁ : ‖1 - A ∘SL DF x₀‖₊ ≤ z₁) (hz₂ : ∀ x ∈ Metric.closedEBall x₀ R, ‖A ∘SL (DF x - DF x₀)‖₊ ≤ z₂ * ‖x - x₀‖₊) {r : NNReal} (hrR : ↑r ≤ R) (hyr : y + z₁ * r + z₂ * r ^ 2 / 2 ≤ r) (hzr : z₁ + z₂ * r < 1) : ∃! x : X, F x = 0 ∧ ‖x - x₀‖₊ ≤ r

Newton--Kantorovich theorem with an explicitly injective approximate inverse.

theorem NewtonKantorovich.surjective {X : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {Y : Type u_3} [NormedAddCommGroup Y] [NormedSpace ℝ Y] {DF : X →L[ℝ] Y} {A : Y →L[ℝ] X} {z₁ : NNReal} (hz₁ : ‖1 - A ∘SL DF‖₊ ≤ z₁) {r : NNReal} (hzr : z₁ + r < 1) : Function.Surjective ⇑A

The approximate inverse is surjective when its composition error is small.

theorem NewtonKantorovich.newton_kantorovich_fd {X : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {Y : Type u_3} [NormedAddCommGroup Y] [NormedSpace ℝ Y] [FiniteDimensional ℝ X] [FiniteDimensional ℝ Y] (hXY : Module.finrank ℝ X = Module.finrank ℝ Y) {F : X → Y} {DF : X → X →L[ℝ] Y} (hF : ∀ (x : X), HasFDerivAt F (DF x) x) (hDF : Continuous DF) {A : Y →L[ℝ] X} {R : ENNReal} {x₀ : X} {y z₁ z₂ : NNReal} (hy : ‖A (F x₀)‖₊ ≤ y) (hz₁ : ‖1 - A ∘SL DF x₀‖₊ ≤ z₁) (hz₂ : ∀ x ∈ Metric.closedEBall x₀ R, ‖A ∘SL (DF x - DF x₀)‖₊ ≤ z₂ * ‖x - x₀‖₊) {r : NNReal} (hrR : ↑r ≤ R) (hyr : y + z₁ * r + z₂ * r ^ 2 / 2 ≤ r) (hzr : z₁ + z₂ * r < 1) : ∃! x : X, F x = 0 ∧ ‖x - x₀‖₊ ≤ r

Finite-dimensional Newton--Kantorovich theorem; equal dimensions make the approximate inverse injective as a consequence of the smallness assumptions.