def IsContraction {X : Type u_1} [MetricSpace X] (f : X → X) : Prop

A self-map f : X → X is a contraction if it is 1-Lipschitz.

def IsStrictContraction {X : Type u_1} [MetricSpace X] (f : X → X) : Prop

A self-map f : X → X is a strict contraction if it has a contraction constant c with 0 < c < 1.

def IsContractionConstant {X : Type u_1} [MetricSpace X] (f : X → X) (c : ℝ) : Prop

A real number c is a contraction constant of f if 0 < c < 1 and dist (f x) (f y) ≤ c * dist x y for all x,y.

theorem definition_6_13 {X : Type u_1} [MetricSpace X] (f : X → X) : (IsContraction f ↔ ∀ (x y : X), dist (f x) (f y) ≤ dist x y) ∧ (IsStrictContraction f ↔ ∃ (c : ℝ), IsContractionConstant f c)

Definition 6.13 (Contraction and strict contraction): (i) f is a contraction iff dist (f x) (f y) ≤ dist x y for all x,y. (ii) f is a strict contraction iff there exists c with 0 < c < 1 such that dist (f x) (f y) ≤ c * dist x y for all x,y; such a c is a contraction constant.

theorem deriv_bound_one_on_interval_implies_nonexpanding {a b : ℝ} (f : ℝ → ℝ) (hmaps : Set.MapsTo f (Set.Icc a b) (Set.Icc a b)) (hcont : ContinuousOn f (Set.Icc a b)) (hdiff : DifferentiableOn ℝ f (Set.Ioo a b)) (hderiv : ∀ x ∈ Set.Ioo a b, |deriv f x| ≤ 1) : (∀ x ∈ Set.Icc a b, ∀ y ∈ Set.Icc a b, |f x - f y| ≤ |x - y|) ∧ IsContraction (Set.MapsTo.restrict f (Set.Icc a b) (Set.Icc a b) hmaps)

Proposition 6.13(1): if f : [a,b] → [a,b] is continuous on [a,b], differentiable on (a,b), and |f'| ≤ 1 on (a,b), then |f(x) - f(y)| ≤ |x - y| for all x,y ∈ [a,b]; in particular, the induced self-map of [a,b] is a non-expanding contraction.

theorem contraction_on_interval_implies_deriv_bound_one {a b : ℝ} (f : ℝ → ℝ) (hdiff : DifferentiableOn ℝ f (Set.Icc a b)) (hcontract : ∀ x ∈ Set.Icc a b, ∀ y ∈ Set.Icc a b, |f x - f y| ≤ |x - y|) (x : ℝ) : x ∈ Set.Icc a b → |derivWithin f (Set.Icc a b) x| ≤ 1

Proposition 6.14: Let f : [a,b] → ℝ be differentiable and assume |f x - f y| ≤ |x - y| for all x,y ∈ [a,b]. Then the derivative of f within [a,b] satisfies |f'(x)| ≤ 1 for all x ∈ [a,b].

theorem helperForProposition_6_15_unpack_nonneg_bound {X : Type u_1} [MetricSpace X] (f : X → X) (hcontract : ∃ (c : ℝ), 0 ≤ c ∧ c < 1 ∧ ∀ (x y : X), dist (f x) (f y) ≤ c * dist x y) : ∃ (c : ℝ), 0 ≤ c ∧ ∀ (x y : X), dist (f x) (f y) ≤ c * dist x y

Helper for Proposition 6.15: from a contraction witness with 0 ≤ c < 1, extract the nonnegativity and distance bound needed for Lipschitz control.

theorem helperForProposition_6_15_lipschitzWith_of_real_contraction_bound {X : Type u_1} [MetricSpace X] (f : X → X) (hbound : ∃ (c : ℝ), 0 ≤ c ∧ ∀ (x y : X), dist (f x) (f y) ≤ c * dist x y) : ∃ (K : NNReal), LipschitzWith K f

Helper for Proposition 6.15: convert a real-valued contraction estimate with c ≥ 0 into an NNReal-valued LipschitzWith bound.

theorem helperForProposition_6_15_continuous_of_exists_lipschitzWith {X : Type u_1} [MetricSpace X] (f : X → X) (hlip : ∃ (K : NNReal), LipschitzWith K f) : Continuous f

Helper for Proposition 6.15: any map with an NNReal Lipschitz bound is continuous.

theorem contraction_has_lipschitz_and_continuous {X : Type u_1} [MetricSpace X] (f : X → X) (hcontract : ∃ (c : ℝ), 0 ≤ c ∧ c < 1 ∧ ∀ (x y : X), dist (f x) (f y) ≤ c * dist x y) : (∃ (K : NNReal), LipschitzWith K f) ∧ Continuous f

Proposition 6.15: If f : X → X on a metric space satisfies dist (f x) (f y) ≤ c * dist x y for some c ∈ [0,1) and all x,y, then f is Lipschitz and therefore continuous on X.

def IsFixedPoint {X : Type u_1} (f : X → X) (x : X) : Prop

Definition 6.14 (Fixed point): Let X be a set and let f : X → X be a map. An element x ∈ X is a fixed point of f if f x = x.

theorem helperForTheorem_6_7_contractingWith_of_nonneg_constant {X : Type u_1} [MetricSpace X] (f : X → X) (hstrict : ∃ (c : ℝ), 0 ≤ c ∧ c < 1 ∧ ∀ (x y : X), dist (f x) (f y) ≤ c * dist x y) : ∃ (K : NNReal), ContractingWith K f

Helper for Theorem 6.7: convert a real-valued contraction bound with 0 ≤ c < 1 into ContractingWith with an NNReal constant.

theorem helperForTheorem_6_7_fixedPoint_eq_of_contractingWith {X : Type u_1} [MetricSpace X] {f : X → X} {K : NNReal} (hfK : ContractingWith K f) {x y : X} (hx : IsFixedPoint f x) (hy : IsFixedPoint f y) : x = y

Helper for Theorem 6.7: fixed points of a ContractingWith map are unique.

theorem helperForTheorem_6_7_existsUnique_fixedPoint_of_contractingWith {X : Type u_1} [MetricSpace X] [Nonempty X] [CompleteSpace X] {f : X → X} {K : NNReal} (hfK : ContractingWith K f) : ∃! x : X, IsFixedPoint f x

Helper for Theorem 6.7: in a nonempty complete metric space, a ContractingWith map has a unique fixed point.

theorem contraction_mapping_theorem_6_7 {X : Type u_1} [MetricSpace X] (f : X → X) (hstrict : ∃ (c : ℝ), 0 ≤ c ∧ c < 1 ∧ ∀ (x y : X), dist (f x) (f y) ≤ c * dist x y) : (∀ (x y : X), IsFixedPoint f x → IsFixedPoint f y → x = y) ∧ (Nonempty X → CompleteSpace X → ∃! x : X, IsFixedPoint f x)

Theorem 6.7 (Contraction mapping theorem): Let (X,d) be a metric space and f : X → X satisfy dist (f x) (f y) ≤ c * dist x y for some c ∈ [0,1) and all x,y. Then f has at most one fixed point. If, in addition, X is nonempty and complete, then f has exactly one fixed point.

theorem helperForProposition_6_16_dist_le_eps_add_c_mul_dist {X : Type u_1} [MetricSpace X] (f g : X → X) (c : ℝ) (x0 y0 : X) (ε : ℝ) (hf : IsContractionConstant f c) (hx0 : IsFixedPoint f x0) (hy0 : IsFixedPoint g y0) (hclose : ∀ (x : X), dist (f x) (g x) ≤ ε) : dist x0 y0 ≤ ε + c * dist x0 y0

Helper for Proposition 6.16: the f-centered triangle inequality and contraction bound imply dist x0 y0 ≤ ε + c * dist x0 y0.

theorem helperForProposition_6_16_dist_le_eps_add_cprime_mul_dist {X : Type u_1} [MetricSpace X] (f g : X → X) (c' : ℝ) (x0 y0 : X) (ε : ℝ) (hg : IsContractionConstant g c') (hx0 : IsFixedPoint f x0) (hy0 : IsFixedPoint g y0) (hclose : ∀ (x : X), dist (f x) (g x) ≤ ε) : dist x0 y0 ≤ ε + c' * dist x0 y0

Helper for Proposition 6.16: the g-centered triangle inequality and contraction bound imply dist x0 y0 ≤ ε + c' * dist x0 y0.

theorem helperForProposition_6_16_le_div_one_sub_of_le_add_mul (d ε a : ℝ) (ha1 : a < 1) (hd : d ≤ ε + a * d) : d ≤ ε / (1 - a)

Helper for Proposition 6.16: from d ≤ ε + a*d with a < 1, one gets d ≤ ε / (1 - a).

theorem helperForProposition_6_16_min_case_finish (d ε c c' : ℝ) (h1 : d ≤ ε / (1 - c)) (h2 : d ≤ ε / (1 - c')) : d ≤ ε / (1 - min c c')

Helper for Proposition 6.16: combine the c- and c'-division bounds into the denominator 1 - min c c' by a case split on c ≤ c'.

theorem fixed_point_distance_le_of_uniformly_close_strict_contractions {X : Type u_1} [MetricSpace X] [CompleteSpace X] (f g : X → X) (c c' : ℝ) (x0 y0 : X) (ε : ℝ) (hf : IsContractionConstant f c) (hg : IsContractionConstant g c') (hx0 : IsFixedPoint f x0) (hy0 : IsFixedPoint g y0) (hε : 0 < ε) (hclose : ∀ (x : X), dist (f x) (g x) ≤ ε) : dist x0 y0 ≤ ε / (1 - min c c')

Proposition 6.16: Let (X,d) be a complete metric space, and let f,g : X → X be strict contractions with contraction constants c,c' ∈ (0,1), respectively. If x₀ and y₀ are fixed points of f and g, and there exists ε > 0 such that dist (f x) (g x) ≤ ε for all x, then dist x₀ y₀ ≤ ε / (1 - min c c').

theorem helperForTheorem_6_6_contractingWith_of_real_constant {X : Type u_1} [MetricSpace X] (f : X → X) (hcontract : ∃ (c : ℝ), 0 < c ∧ c < 1 ∧ ∀ (x y : X), dist (f x) (f y) ≤ c * dist x y) : ∃ (K : NNReal), ContractingWith K f

Helper for Theorem 6.6: turn the real-valued contraction hypothesis into ContractingWith with an NNReal constant.

theorem helperForTheorem_6_6_isFixedPoint_iff_isFixedPt {X : Type u_1} (f : X → X) (x : X) : IsFixedPoint f x ↔ Function.IsFixedPt f x

Helper for Theorem 6.6: the local fixed-point predicate agrees with mathlib's IsFixedPt.

theorem helperForTheorem_6_6_unique_at_mathlib_fixedPoint {X : Type u_1} [MetricSpace X] [CompleteSpace X] [Nonempty X] {f : X → X} {K : NNReal} (hfK : ContractingWith K f) (y : X) : IsFixedPoint f y → y = ContractingWith.fixedPoint f hfK

Helper for Theorem 6.6: uniqueness stated using ContractingWith.fixedPoint.

theorem helperForTheorem_6_6_tendsto_nat_iterate_fixedPoint {X : Type u_1} [MetricSpace X] [CompleteSpace X] [Nonempty X] {f : X → X} {K : NNReal} (hfK : ContractingWith K f) (x0 : X) : Filter.Tendsto (fun (n : ℕ) => f^[n] x0) Filter.atTop (nhds (ContractingWith.fixedPoint f hfK))

Helper for Theorem 6.6: iterates Nat.iterate f n x₀ converge to the ContractingWith.fixedPoint.

theorem banach_fixed_point_theorem {X : Type u_1} [MetricSpace X] [CompleteSpace X] [Nonempty X] (f : X → X) (hcontract : ∃ (c : ℝ), 0 < c ∧ c < 1 ∧ ∀ (x y : X), dist (f x) (f y) ≤ c * dist x y) : ∃ (xstar : X), IsFixedPoint f xstar ∧ (∀ (y : X), IsFixedPoint f y → y = xstar) ∧ ∀ (x0 : X), Filter.Tendsto (fun (n : ℕ) => f^[n] x0) Filter.atTop (nhds xstar)

Theorem 6.6 (Banach fixed-point theorem): If X is a nonempty complete metric space and f : X → X is a contraction with constant c satisfying 0 < c < 1, then f has a unique fixed point x*; moreover, for every initial point x₀, the iterates x_{n+1} = f(x_n) converge to x*.