2.1.lean

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

/-- 这个结构体持有PL定理所需的所有参数。 -/
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
  }⟩



/-- 证明 FunSpace 的相等性。-/
@[ext]
lemma FunSpace.ext {f g : FunSpace v}
  (h : ∀ x : v.iccr, f.toFun x = g.toFun x) :
  f = g :=
by
  -- 解构 f, g
  cases f; cases g
  -- FunSpace 有哪些字段，就对每个字段分别做相等性证明
  congr
  -- 对函数字段则用 funext
  funext x
  exact h x
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


instance : CompleteSpace v.FunSpace where
  complete := by
    sorry

/-- 定义压缩映射。 -/
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
/-- 证明 T 是压缩映射：存在常数 C = K * r 且 C < 1，使得对所有 f, g 有
dist (T f, T g) ≤ C * dist (f, g) 。 -/
theorem T_contract : ∃ C, ContractingWith C (T : FunSpace v → FunSpace v) :=
by
  sorry

end FunSpace

/-- 存在不动点 -/
theorem exists_unique_fixed : ∃! f : FunSpace v, f.T = f := by
  obtain ⟨K, hT⟩ := FunSpace.T_contract (E := E)
  -- `f`是压缩映射`T`的不动点，
  let f : FunSpace v := ContractingWith.fixedPoint _ hT
  -- `hf_isFixedPt`是对应的证明。
  have hf_isFixedPt := ContractingWith.fixedPoint_isFixedPt hT
  -- 不动点的唯一性证明。
  have hf_unique : ∀ g, Function.IsFixedPt (FunSpace.T : FunSpace v → FunSpace v) g → g = f := by
    intro g hg
    exact ContractingWith.fixedPoint_unique hT hg
  exact ⟨_, hf_isFixedPt, hf_unique⟩
end MyPL

open MyPL

theorem picard_lindelof_theorem {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
[CompleteSpace E] [FiniteDimensional ℝ E]
    (b : ℝ → E → E) (t₀ : ℝ) (x₀ : E) (α β K M r : ℝ≥0)
    {hp: IsPL b t₀ x₀ α β K M r} : ∃! γ : FunSpace ⟨b, t₀, x₀, α, β, K, M, r, hp⟩, γ.T = γ := by
  exact exists_unique_fixed ⟨b, t₀, x₀, α, β, K, M, r, hp⟩