def contraction {X : Type u} [PseudoMetricSpace X] {Y : Type v} [PseudoMetricSpace Y] (φ : X → Y) : Prop

Definition 7.6.1. A map φ : X → Y between metric spaces is a contraction if it is k-Lipschitz for some k < 1, i.e., there exists k < 1 such that dist (φ p) (φ q) ≤ k * dist p q for all p, q. For a self-map φ : X → X, a point x is a fixed point when φ x = x.

Equations

• contraction φ = ∃ (k : NNReal), ↑k < 1 ∧ LipschitzWith k φ

def fixedPoint {X : Type u} (φ : X → X) (x : X) : Prop

Equations

• fixedPoint φ x = (φ x = x)

theorem fixedPoint_iff_isFixedPt {X : Type u} (φ : X → X) (x : X) : fixedPoint φ x ↔ Function.IsFixedPt φ x

The book's fixed point notion coincides with Function.IsFixedPt.

theorem contraction_unique_fixedPoint (X : Type u) [MetricSpace X] [CompleteSpace X] [Nonempty X] (φ : X → X) (hφ : contraction φ) : ∃! x : X, fixedPoint φ x

Theorem 7.6.2 (contraction mapping principle or Banach fixed point theorem). If (X, d) is a nonempty complete metric space and φ : X → X is a contraction, then φ has a unique fixed point.

theorem metric_picard_existence_uniqueness {a b c d x₀ y₀ L : ℝ} (hI : a ≤ b) (hJ : c ≤ d) (hx₀ : x₀ ∈ Set.Ioo a b) (hy₀ : y₀ ∈ Set.Ioo c d) (F : ℝ → ℝ → ℝ) (hF_cont : ContinuousOn (fun (p : ℝ × ℝ) => F p.1 p.2) (Set.Icc a b ×ˢ Set.Icc c d)) (hL_nonneg : 0 ≤ L) (hF_lip : ∀ x ∈ Set.Icc a b, ∀ y ∈ Set.Icc c d, ∀ z ∈ Set.Icc c d, |F x y - F x z| ≤ L * |y - z|) : ∃ h > 0, Set.Icc (x₀ - h) (x₀ + h) ⊆ Set.Icc a b ∧ ∃ (f : ℝ → ℝ), DifferentiableOn ℝ f (Set.Icc (x₀ - h) (x₀ + h)) ∧ (∀ x ∈ Set.Icc (x₀ - h) (x₀ + h), f x ∈ Set.Icc c d) ∧ f x₀ = y₀ ∧ (∀ x ∈ Set.Icc (x₀ - h) (x₀ + h), HasDerivAt f (F x (f x)) x) ∧ ∀ (g : ℝ → ℝ), DifferentiableOn ℝ g (Set.Icc (x₀ - h) (x₀ + h)) → (∀ x ∈ Set.Icc (x₀ - h) (x₀ + h), g x ∈ Set.Icc c d) → g x₀ = y₀ → (∀ x ∈ Set.Icc (x₀ - h) (x₀ + h), HasDerivAt g (F x (g x)) x) → Set.EqOn g f (Set.Icc (x₀ - h) (x₀ + h))

Theorem 7.6.3 (Picard's theorem on existence and uniqueness). Let I = [a, b] and J = [c, d] be closed bounded intervals in ℝ with x₀ ∈ (a, b) and y₀ ∈ (c, d). Suppose F : ℝ → ℝ → ℝ is continuous on I × J and Lipschitz in the second variable with Lipschitz constant L, meaning |F x y - F x z| ≤ L * |y - z| for all x ∈ I and y, z ∈ J. Then there exists h > 0 with [x₀ - h, x₀ + h] ⊆ I and a unique differentiable function f : ℝ → ℝ with values in J such that f x₀ = y₀ and f' x = F x (f x) on [x₀ - h, x₀ + h].