How to define a contraction map in my example.

Stream: lean4

[liuzi]

import Mathlib
open NNReal Set
/-- IsPicardLindelof in finite dimensional real vector space -/
structure IsPL {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
[CompleteSpace E] [FiniteDimensional ℝ E]
    (b : ℝ → E → E) (t₀ : ℝ) (x₀ : E) (α β K M r : ℝ≥0) : Prop where
  cont : ∀ x, ‖x - x₀‖ ≤ β → ContinuousOn (fun t : ℝ => b t x) (Icc (t₀ - α) (t₀ + α))
  lipschitz : ∀ t ∈ Icc (t₀ - α) (t₀ + α), LipschitzOnWith K (b t) {x | ‖x - x₀‖ ≤ β}
  norm_le : ∀ t ∈ Icc (t₀ - α) (t₀ + α), ∀ x, ‖x - x₀‖ ≤ β → ‖b t x‖ ≤ M
  K_nezero : K ≠ 0
  r_lt : r < α ⊓ β / M ⊓ 1 / K

/-- all parameters -/
structure MyPL (E : Type*) [NormedAddCommGroup E] [NormedSpace ℝ E]
[CompleteSpace E] [FiniteDimensional ℝ E] where
  b : ℝ → E → E
  t₀ : ℝ
  x₀ : E
  (α β K M r : ℝ≥0)
  isPL : IsPL b t₀ x₀ α β K M r

namespace MyPL

variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
[CompleteSpace E] [FiniteDimensional ℝ E]
variable (v : MyPL E)

/-- Defines the closed interval `[t₀ - r, t₀ + r]`. -/
def iccr : Set ℝ := Icc (v.t₀ - v.r) (v.t₀ + v.r)

/-- Clearly, `t₀` belongs to the closed interval `[t₀ - r, t₀ + r]`. -/
lemma t₀_mem_iccr : v.t₀ ∈ v.iccr := by unfold iccr; simp

def t₀_iccr : v.iccr := ⟨_, v.t₀_mem_iccr⟩

structure FunSpace where
  toFun : v.iccr → E
  map_t₀' : toFun v.t₀_iccr = v.x₀
  norm_le_β : ∀ t : v.iccr, ‖toFun t - v.x₀‖ ≤ v.β
  continuous: Continuous toFun
/-- Implementing Inhabited because we need FunSpace to be nonempty
in order to guarantee the existence of a fixed point. -/
instance : Inhabited (FunSpace v) :=
  ⟨{ toFun := λ _ => v.x₀
     map_t₀' := by simp [t₀_iccr]
     norm_le_β := by simp
     continuous := by continuity
  }⟩


namespace FunSpace

variable {v}
variable (f g: FunSpace v)
-- # Prove FunSpace is a Metric Space
noncomputable instance : MetricSpace v.FunSpace where
  dist f g := ⨆ (t : v.iccr), ‖f.toFun t - g.toFun t‖
  dist_self f := by simp [dist]
  dist_comm f g := by simp [dist, norm_sub_rev]
  dist_triangle f g h := by
    sorry
  eq_of_dist_eq_zero := by sorry

/-- Defines a contraction map. -/
def T (f : FunSpace v) : FunSpace v where
  toFun := λ t => v.b t (f.toFun t)
  map_t₀' := by
    sorry
  norm_le_β := by
    sorry
  continuous := by
    sorry
end FunSpace

end MyPL