1.lean

import Mathlib

set_option autoImplicit false

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₀
  lipschitz' : LipschitzWith v.K 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 := fun _ => v.x₀
     map_t₀' := by simp [t₀_iccr]
     lipschitz' := LipschitzWith.const' v.x₀}⟩


@[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
    simp only [dist, iSup_le_iff]
    intro x
    cases x with t ht
    exact le_trans (norm_sub_le _ _) (add_le_add (le_iSup_of_le t (le_iSup_of_le ht (le_refl _)))
    (le_iSup_of_le t (le_iSup_of_le ht (le_refl _))))
  eq_of_dist_eq_zero h := by
    ext ⟨t, ht⟩
    have h' := congr_fun (congr_arg FunSpace.toFun h) ⟨t, ht⟩
    simp_all [dist]

instance : CompleteSpace v.FunSpace where
  refine' Metric.complete_of_convergent_controlled_sequences (fun n => (1 / 2) ^ n) _ _
  · intro n
    exact half_pos (one_pos)
  · intro f hf
    have h_cau : CauchySeq f := cauchySeq_of_dist_le_of_summable _ hf (summable_geometric_two)
    obtain ⟨γ, hγ⟩ := cauchySeq_tendsto_of_complete h_cau
    refine' ⟨γ, _⟩
    exact tendsto_nhds_of_eventually_eq hγ (eventually_of_forall fun n => _)
    -- We need to prove that the sequence converges to γ, and that γ satisfies the conditions of FunSpace.
-- Further elaboration is required here, utilizing the preservation properties of uniform convergence and the Lipschitz condition.
    <;> simp_all [dist]
    <;> linarith

/-- 定义压缩映射。 -/
def T (f : FunSpace v) : FunSpace v where
  toFun := fun t => v.x₀ + ∫ τ in v.t₀..t.1, v.b τ (f.toFun ⟨τ, by linarith [v.isPL.r_lt.1, v.isPL.r_lt.2.1, t.2.1, t.2.2]⟩)
  map_t₀' := by simp [v.isPL.r_lt.1]
  lipschitz' := by
    -- 需要证明T(f)是Lipschitz的，利用b的Lipschitz条件和积分估计
    apply LipschitzWith.of_dist_le_mul
    intro t₁ t₂
    simp [dist_eq_norm, norm_sub_rev]
    calc
      ‖∫ τ in v.t₀..t₁.1, v.b τ (f.toFun ⟨τ, _⟩) - ∫ τ in v.t₀..t₂.1, v.b τ (f.toFun ⟨τ, _⟩)‖ ≤
          ‖∫ τ in v.t₀..t₁.1, v.b τ (f.toFun ⟨τ, _⟩) - v.b τ (f.toFun ⟨τ, _⟩)‖ + ‖∫ τ in t₁.1..t₂.1, v.b τ (f.toFun ⟨τ, _⟩)‖ :=
        by simp [integral_sub, integral_add]
      _ ≤ v.K * dist f f * |t₁.1 - t₂.1| + v.M * |t₁.1 - t₂.1| := by
        -- 应用Lipschitz条件和范数估计
        gcongr <;> simp_all [v.isPL.lipschitz, v.isPL.norm_le]
      _ ≤ (v.K * 1 + v.M) * |t₁.1 - t₂.1| := by ring
      _ ≤ (v.K + v.M) * |t₁.1 - t₂.1| := by linarith

/-- 证明映射`T`是压缩映射。 -/
theorem T_contract : ∃ K, ContractingWith K (T : FunSpace v → FunSpace v) := by
  use v.K * v.r
  constructor
  · -- 证明压缩常数K < 1
    linarith [v.isPL.r_lt.2.2]
  · -- 证明T是压缩的
    intro f g
    simp [dist_eq_iSup, T]
    calc
      ⨆ t ∈ v.iccr, ‖(T f).toFun t - (T g).toFun t‖ ≤ ⨆ t ∈ v.iccr, v.K * v.r * ‖f.toFun t - g.toFun t‖ := by
        -- 应用积分估计和Lipschitz条件
        refine' iSup_le fun t => iSup_le fun ht => _
        simp_all [v.isPL.lipschitz, integral_sub, integral_mul_left]
        <;> linarith [v.isPL.r_lt.1, v.isPL.r_lt.2.1, v.isPL.r_lt.2.2]
      _ ≤ v.K * v.r * ⨆ t ∈ v.iccr, ‖f.toFun t - g.toFun t‖ := by
        -- 提取常数因子
        simp [mul_iSup]
      _ = v.K * v.r * dist f g := by
        -- 根据度量定义
        simp [dist_eq_iSup]

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} :
    ∃! γ  : ℝ → E, γ t₀ = x₀ ∧
    ∀ t ∈ Icc (t₀ - r) (t₀ + r), HasDerivWithinAt γ (b t (γ t)) (Icc (t₀ - α) (t₀ + α)) t := by
    let X := {γ | ContinuousOn γ (Icc (t₀ - r) (t₀ + r)) ∧ γ t₀ = x₀ ∧ ∀ t ∈ Icc (t₀ - r) (t₀ + r), ‖γ t - x₀‖ ≤ β}
    let T : X → X := λ γ t x₀ + ∫ τ in t₀..t, b τ (γ τ) ∂τ
    have hX_metric : MetricSpace X := inferInstance
    have hX_complete : CompleteSpace X := inferInstance
    have hT_contract : ContractingWith K T := by
    -- 应用之前的T_contract定理
      exact T_contract (E := E) ⟨b, t₀, x₀, α, β, K, M, r, hp⟩
    obtain ⟨γ, hγ⟩ := ContractingWith.exists_fixedPoint hT_contract
    refine' ⟨γ, _⟩
    -- 验证γ满足初始条件和微分方程
    simp_all [HasDerivWithinAt, hT_contract.fixedPoint_isFixedPt]
    <;> linarith [hp.r_lt.1, hp.r_lt.2.1, hp.r_lt.2.2]
    /--/
     let X := {γ | ContinuousOn γ iccr ∧ γ t₀ = x₀ ∧ ∀ t ∈ iccr, ‖γ t - x₀‖ ≤ β}
     let T : X → X := λ γ t, x₀ + ∫ t₀ to t, b s (γ s) ds
     X is metric space := sorry
     X is complete space := sorry
     have T γ t₀ = x₀ := sorry
     have ∀t∈ iccr, T γ t - x₀ ≤ β :=
     calc ‖T γ t - x₀ ‖≤ ∫ t₀ to t, ‖b s (γ s)‖ ds : sorry
                       ≤ M * (t - t₀) : sorry
                       ≤ M * r : sorry
                       ≤ β : sorry


      have ∀γ₁ γ₂ ∈ X, ∃L∈ (0,1), ‖T γ₁ t - T γ₂ t‖ ≤ Kr ‖γ₁ - γ₂‖ :=
      intro γ₁ γ₂
      use Kr
      calc ‖T γ₁ t - T γ₂ t‖ = ∫ t₀ to t, ‖b s (γ₁ s) - b s (γ₂ s)‖ ds : sorry
                            ≤ ∫ t₀ to t, K * ‖γ₁ s - γ₂ s‖ ds : sorry
                            ≤ K * ‖γ₁ - γ₂‖ : sorry
                            ≤ Kr ‖γ₁ - γ₂‖ : sorry


  -- # 利用banach fixed point theorem证明T有唯一的fixed point
  --   have T has a unique fixed point := by
  --   Banach_fixed_point_theorem
  sorry