2.2.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
  M_nezero : M ≠ 0
  α_nezero : α ≠ 0
  β_nezero : β ≠ 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]`. -/
abbrev 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}

/-- Coerce `FunSpace` to `[t₀-r,t₀+r] → E`. This can simplify the code. -/
instance : CoeFun (FunSpace v) fun _ => v.iccr → E :=
  ⟨toFun⟩

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

/-- If function `f : ι → ℝ` is bounded above then for all `i` we have `f i ≤ ⨆ i, f i`. -/
lemma Real.le_iSup_of_bddAbove {ι : Type*} [Nonempty ι] {f : ι → ℝ} (h : BddAbove (Set.range f)) (i : ι) :
    f i ≤ ⨆ i, f i := by
  change f i ≤ sSup (Set.range f)
  suffices IsLUB (Set.range f) (sSup (Set.range f)) from this.1 (by simp)
  exact Real.isLUB_sSup (range_nonempty f) h

/-- Make `v.iccr` inhabited, as a consequnce `v.iccr` is `Nonempty`. -/
instance : Inhabited v.iccr := ⟨v.t₀_iccr⟩

/-- For `f, g` in `FunSpace` we have `‖f(t) - g(t)‖ ≤ 2β`. -/
lemma funSpace_sub_le (f g : FunSpace v) (t : v.iccr) : ‖f t - g t‖ ≤ 2 * v.β := calc
  _ = ‖f t - v.x₀ - (g t - v.x₀)‖ := by congr 1; abel
  _ ≤ ‖f t - v.x₀‖ + ‖g t - v.x₀‖ := norm_sub_le ..
  _ ≤ v.β + v.β := by gcongr <;> apply FunSpace.norm_le_β
  _ = _ := by rw [two_mul]

/-- `‖f(t) - g(t)‖` is bounded. -/
lemma funSpace_sub_bddAbove (f g : FunSpace v) : BddAbove (Set.range (fun t => ‖f t - g t‖)) := by
  use 2 * v.β
  intro t ⟨f, hf⟩
  rw [← hf]
  exact funSpace_sub_le ..

/-- For `f, g` in `FunSpace` we have `0 ≤ ⨆ t, ‖f(t) - g(t)‖`. -/
lemma funSpace_iSup_sub_nonneg (f g : FunSpace v) : 0 ≤ ⨆ t, ‖f t - g t‖ := by
  apply Real.iSup_nonneg'
  use default
  exact norm_nonneg _

-- # Prove FunSpace is a Metric Space
noncomputable instance : MetricSpace v.FunSpace where
  dist f g := ⨆ (t : v.iccr), ‖f t - g t‖
  dist_self f := by simp [dist]
  dist_comm f g := by simp [dist, norm_sub_rev]
  dist_triangle f g h := by
    simp [dist]
    refine Real.iSup_le (fun t => ?_)
      (add_nonneg (funSpace_iSup_sub_nonneg ..) (funSpace_iSup_sub_nonneg ..))
    calc
      _ = ‖f t - g t + (g t - h t)‖ := by congr 1; abel
      _ ≤ ‖f t - g t‖ + ‖g t - h t‖ := norm_add_le ..
      _ ≤ _ := by
        gcongr
        . apply Real.le_iSup_of_bddAbove (f := fun t => ‖f t - g t‖)
          exact funSpace_sub_bddAbove ..
        . apply Real.le_iSup_of_bddAbove (f := fun t => ‖g t - h t‖)
          exact funSpace_sub_bddAbove ..
  eq_of_dist_eq_zero := by
    intro x y hxy
    -- Use `ext` lemma
    ext t
    rw [← sub_eq_zero]
    -- Suffices to show `‖x(t) - y(t)‖ = 0`
    suffices ‖x t - y t‖ = 0 by rwa [norm_eq_zero] at this
    -- Suffices to show `‖x(t) - y(t)‖ ≤ 0`
    refine le_antisymm ?_ (by positivity)
    -- Notice that `⨆ t, ‖x(t) - y(t)‖ = 0` suffices to show `‖x(t) - y(t)‖ ≤ ⨆ t, ‖x(t) - y(t)‖`.
    simp [← hxy]
    -- `‖x(t) - y(t)‖ ≤ ⨆ t, ‖x(t) - y(t)‖` holds since `‖x(t)-y(t)‖ ≤ 2β`
    apply Real.le_iSup_of_bddAbove (f := fun t => ‖x t - y t‖)
    exact funSpace_sub_bddAbove ..


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


/-- 定义压缩映射。 -/
noncomputable def T (f : FunSpace v) : FunSpace v where
  toFun := fun t => v.x₀ + ∫ s in v.t₀..t, v.b s (f ⟨s, _⟩)
  map_t₀' := by
    simp [t₀_iccr]
  norm_le_β := by
    intro t
    calc  ‖(v.x₀ + ∫ s in v.t₀..t, v.b s (f ⟨s, _⟩)) - v.x₀‖ = ‖∫ s in v.t₀..t, v.b s (f ⟨s, _⟩)‖ := by simp
          _≤ ∫ s in v.t₀..t, ‖v.b s (f ⟨s, _⟩)‖ := sorry
          _≤ ∫ s in v.t₀..t, v.M := sorry
          _= v.M * (t - v.t₀):= sorry
          _≤ v.β:= sorry
  continuous := by
    apply continuous_const.add
    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
  use v.K * v.r
  rw [ContractingWith]
  constructor
  sorry
  rw [LipschitzWith]
  intro f g
  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⟩