2.3.lean

import Mathlib
open NNReal Set Classical
suppress_compilation

  /-- 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 < α
  r_lt_β_M : r < β / M
  r_lt_K : r < 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)

-- 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

/-- Defines the closed interval `[t₀ - r, t₀ + r]`. -/

abbrev iccr : Set ℝ := Icc (v.t₀ - v.r) (v.t₀ + v.r)

lemma mem_iccr_iff {t : ℝ} : t ∈ v.iccr ↔ |t - v.t₀| ≤ v.r := by
  delta iccr
  rw [abs_le]
  simp only [mem_Icc, tsub_le_iff_right, neg_le_sub_iff_le_add, and_congr_right_iff]
  intro h
  fconstructor
  · intro h; linarith
  · intro h; linarith

/-- 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⟩

abbrev FunSpace := {f : ContinuousMap v.iccr E //f v.t₀_iccr = v.x₀ ∧ ∀ t : v.iccr, ‖f t - v.x₀‖ ≤ v.β}

instance : FunLike (FunSpace v) v.iccr E where
  coe f := f.1
  coe_injective' f g h := by
    simp only [DFunLike.coe_fn_eq] at h
    ext x
    exact congr($h x)

lemma FunSpace.cont (f : FunSpace v) : Continuous (fun x : v.iccr ↦ v.b x (f x)) := by
  sorry

-- structure FunSpace extends ContinuousMap v.iccr E 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) :=
  ⟨{
    val :=
    { toFun t := v.x₀
      continuous_toFun := by continuity }
    property :=
    { left := by simp
      right := by simp }
  }⟩

-- variable {v} in
-- def FunSpace.toFun (f : FunSpace v) : v.iccr → E := f.1

variable {v} in
def FunSpace.map_t₀' (f : FunSpace v)  : f.1 v.t₀_iccr = v.x₀ := f.2.1

variable {v} in
def FunSpace.norm_le_β (f : FunSpace v) : ∀ t : v.iccr, ‖f t - v.x₀‖ ≤ v.β := f.2.2

@[continuity]
lemma FunSpace.continuous (f : FunSpace v) : Continuous f := f.1.continuous

lemma FunSpace.bddAbove (f : FunSpace v) : BddAbove (range fun t ↦ ‖f t‖) := by
  rw [← Set.image_univ]
  apply IsCompact.bddAbove_image
  · exact CompactSpace.isCompact_univ
  rw [← continuous_iff_continuousOn_univ]
  continuity

variable {v} in
def FunSpace.extended (f : FunSpace v) : ℝ → E := fun x => if h : x ∈ v.iccr then f ⟨x, h⟩ else 0

lemma extended_apply_of_mem (f : FunSpace v) (x : v.iccr) :  f.extended x = f x := by
  simp [FunSpace.extended, x.property]

lemma extended_apply_of_not_mem (f : FunSpace v) (x : ℝ) (hx : x ∉ v.iccr) : f.extended x = 0 := by
  simp [FunSpace.extended, hx]

lemma extended_integrable (f : FunSpace v) (t  : v.iccr) :
    IntervalIntegrable (fun s ↦ v.b s (f.extended s)) MeasureTheory.volume v.t₀ t.1 := by
  rw [intervalIntegrable_iff']
  apply ContinuousOn.integrableOn_uIcc
  sorry

@[ext]
lemma FunSpace.ext {f g : FunSpace v}
  (h : ∀ x : v.iccr, f.1 x = g.1 x) :
  f = g := DFunLike.ext f g h

namespace FunSpace

variable {v}
variable (f g: FunSpace v)

-- # Prove FunSpace is a Metric Space
instance : MetricSpace v.FunSpace := inferInstance

lemma FunSpace.dist_apply (f g : FunSpace v) : dist f g = ⨆ (t : v.iccr), ‖f t - g t‖ := by
  change dist f.1 g.1 = _
  rw [dist_eq_norm]
  exact ContinuousMap.norm_eq_iSup_norm _


lemma FunSpace.edist_apply (f g : FunSpace v) : edist f g = ENNReal.ofNNReal ⟨dist f g, dist_nonneg⟩ := rfl

lemma iccr_eq_uIcc : v.iccr = uIcc (v.t₀ - v.r) (v.t₀ + v.r) := by
  rw [uIcc_of_le]
  rw [sub_le_iff_le_add, add_assoc]
  have : 0 ≤ v.r.1 := by exact v.r.2
  apply le_add_of_nonneg_right
  positivity

instance : CompleteSpace v.FunSpace := by
  apply IsClosed.completeSpace_coe
  apply IsSeqClosed.isClosed
  intro rn r hrn hr
  constructor
  · show r v.t₀_iccr = v.x₀
    sorry
  show ∀ (t: ↑v.iccr), ‖r t - v.x₀‖ ≤ ↑v.β
  intro t
  sorry

/-- define contraction map -/
def T (f : FunSpace v) : FunSpace v where
  val :=
  { toFun := fun t => v.x₀ + ∫ s in v.t₀..t, v.b s (f.extended s)
    continuous_toFun := by
      have : ContinuousOn (fun t : ℝ ↦ ∫ s in v.t₀..t, v.b s (f.extended s)) (uIcc (v.t₀ - v.r) (v.t₀ + v.r)):= by
        apply intervalIntegral.continuousOn_primitive_interval'
        rw [intervalIntegrable_iff']
        -- -- intro a b
        apply ContinuousOn.integrableOn_uIcc
        · rw [uIcc_of_le]
          · rw [continuousOn_iff_continuous_restrict]
            rw [show (Icc (v.t₀ - ↑v.r) (v.t₀ + ↑v.r)).restrict (fun x ↦ v.b x (f.extended x)) = fun x : v.iccr ↦ v.b x (f x) by
              ext x
              simp [extended_apply_of_mem]]
            apply FunSpace.cont
          · rw [sub_le_iff_le_add, add_assoc]
            have : 0 ≤ v.r.1 := by exact v.r.2
            apply le_add_of_nonneg_right
            positivity
        rw [← iccr_eq_uIcc]
        simp only [mem_Icc, tsub_le_iff_right, le_add_iff_nonneg_right, zero_le_coe, and_self]
      have : ContinuousOn (fun t : ℝ ↦ ∫ s in v.t₀..t, v.b s (f.extended s)) (v.iccr):= by
        apply this.mono
        rw [iccr_eq_uIcc]
      have : Continuous fun t : v.iccr ↦ ∫ s in v.t₀..t, v.b s (f.extended s) := by
        exact this.restrict


      refine Continuous.add continuous_const this }
  property := {
    left := by simp [t₀_iccr]
    right := by
      intro t
      calc  ‖(v.x₀ + ∫ s in v.t₀..t, v.b s  (f.extended s)) - v.x₀‖
            _ = ‖∫ s in v.t₀..t, v.b s (f.extended s)‖ := by simp
            _ ≤ ‖∫ s in v.t₀..t, ‖v.b s (f.extended s)‖‖ := intervalIntegral.norm_integral_le_abs_integral_norm ..
            _ ≤ ‖∫ s in v.t₀..t, v.M.1‖ := by
              conv_rhs => simp only [Real.norm_eq_abs, val_eq_coe, intervalIntegral.integral_const, smul_eq_mul,
                norm_mul, NNReal.abs_eq]
              rw [mul_comm]
              apply intervalIntegral.norm_integral_le_of_norm_le_const_ae
              apply Filter.Eventually.of_forall
              intro x hx

              have mem : x ∈ v.iccr := by
                by_cases ht : v.t₀ ≤ t
                · rw [uIoc_of_le ht] at hx
                  simp only [iccr, mem_Ioc, mem_Icc, tsub_le_iff_right] at hx ⊢
                  constructor
                  · linarith [show 0 ≤ (v.r : ℝ) from v.r.2]
                  · exact le_trans hx.2 t.2.2
                · rw [uIoc_of_ge (le_of_lt <| by simpa using ht)] at hx
                  simp only [iccr, mem_Ioc, mem_Icc, tsub_le_iff_right] at hx ⊢
                  constructor
                  · suffices v.t₀ - v.r ≤ x by linarith
                    exact le_trans t.2.1 hx.1.le
                  · linarith[show 0 ≤ (v.r : ℝ) from v.r.2]
              simp only [norm_norm] at hx ⊢
              apply v.isPL.norm_le x
              · have : v.iccr ⊆ Icc (v.t₀ - ↑v.α) (v.t₀ + ↑v.α) := by
                  simp only [iccr]
                  have : v.r.1 < v.α.1 := v.isPL.r_lt_α

                  refine Icc_subset_Icc ?_ ?_
                  · apply sub_le_sub_left
                    exact le_of_lt this

                  · apply add_le_add_left
                    exact le_of_lt this
                exact this mem

              ·
                rw [extended_apply_of_mem v f ⟨x, mem⟩]
                exact FunSpace.norm_le_β f ⟨x, mem⟩
            _ = v.M * |t - v.t₀|:= by simp [mul_comm]
            _ ≤ v.β:= by
              have : 0 < (v.M: ℝ) := by
                rw[lt_iff_le_and_ne]
                exact ⟨v.M.2, by symm; exact_mod_cast v.isPL.M_nezero⟩
              suffices |t - v.t₀| ≤ v.β / v.M by
                rwa [le_div_iff₀ (show 0 < (v.M: ℝ) by assumption), mul_comm] at this
              have : (v.r : ℝ) < v.β / v.M := v.isPL.r_lt_β_M
              refine le_trans ?_ this.le
              rw[abs_le]
              constructor <;>  linarith [t.2.1, t.2.2]


  }

lemma T_apply (f : FunSpace v) (t : v.iccr) : f.T t = v.x₀ + ∫ s in v.t₀..t, v.b s (f.extended s) := rfl
-- where
--   toFun := fun t => v.x₀ + ∫ s in v.t₀..t, v.b s (extended _ f s)
--   map_t₀' := by
--     simp [t₀_iccr]
--   norm_le_β := by
--     intro t
--     calc  ‖(v.x₀ + ∫ s in v.t₀..t, v.b s  (extended _ f s)) - v.x₀‖
--           _ = ‖∫ s in v.t₀..t, v.b s (f.1 ⟨s, sorry⟩)‖ := by simp
--           _ ≤ ∫ s in v.t₀..t, ‖v.b s (f.1 ⟨s, sorry⟩)‖ := sorry
--           _ ≤ ∫ s in v.t₀..t, v.M.1 := sorry
--           _ = v.M * (t - v.t₀):= sorry
--           _ ≤ v.β:= sorry
--   continuous := by
--     sorry
instance : Nonempty v.iccr := ⟨v.t₀_iccr⟩
-- theorem mem_iccr_of_mem_uIoc (t : v.iccr) {x : ℝ} (hx : x ∈ uIoc v.t₀ t) : x ∈ v.iccr := by
--   by_cases ht : v.t₀ ≤ t
--   · rw [uIoc_of_le ht] at hx
--     simp only [iccr, mem_Ioc, mem_Icc, tsub_le_iff_right] at hx ⊢
--     constructor
--     . linarith [show 0 ≤ (v.r : ℝ) from v.r.2]
--     . exact le_trans hx.2 t.2.2
--   · rw [uIoc_of_ge (le_of_lt <| by simpa using ht)] at hx
--     simp only [iccr, mem_Ioc, mem_Icc, tsub_le_iff_right] at hx ⊢
--     constructor
--     . suffices v.t₀ - v.r ≤ x by linarith
--       exact le_trans t.2.1 hx.1.le
--     . linarith [show 0 ≤ (v.r : ℝ) from v.r.2]
lemma sub_norm_le (f : FunSpace v) (t : v.iccr) : ‖v.b t (f.extended t)‖ ≤ v.M := by
  rw [extended_apply_of_mem]
  apply v.isPL.norm_le
  . constructor
    . refine le_trans ?_ t.2.1
      linarith [show (v.r : ℝ) ≤ v.α from v.isPL.r_lt_α.le]
    . refine le_trans t.2.2 ?_
      linarith [show (v.r : ℝ) ≤ v.α from v.isPL.r_lt_α.le]
  exact norm_le_β f t

lemma dist_T (f g : FunSpace v) : dist f.T g.T ≤ v.K * v.r * (dist f g) := by
  rw [FunSpace.dist_apply]
  rw [ciSup_le_iff]
  · intro t
    simp only [T_apply, add_sub_add_left_eq_sub]
    rw [← intervalIntegral.integral_sub]


    . trans ‖∫ (x : ℝ) in v.t₀..↑t, ‖v.b x (f.extended x) - v.b x (g.extended x)‖‖
      · exact intervalIntegral.norm_integral_le_abs_integral_norm ..
      calc ‖∫ (x : ℝ) in v.t₀..↑t, ‖v.b x (f.extended x) - v.b x (g.extended x)‖‖
        _ ≤ |t - v.t₀| * ⨆ (t : v.iccr), ‖v.b t (f.extended t) - v.b t (g.extended t)‖ := by
          rw [mul_comm]
          apply intervalIntegral.norm_integral_le_of_norm_le_const_ae
          apply Filter.Eventually.of_forall
          intro x hx
          rw[norm_norm]
          have x_mem : x ∈ v.iccr := by
            by_cases ht : v.t₀ ≤ t
            · rw [uIoc_of_le ht] at hx
              simp only [iccr, mem_Ioc, mem_Icc, tsub_le_iff_right] at hx ⊢
              constructor
              · linarith [show 0 ≤ (v.r : ℝ) from v.r.2]
              · exact le_trans hx.2 t.2.2
            · rw [uIoc_of_ge (le_of_lt <| by simpa using ht)] at hx
              simp only [iccr, mem_Ioc, mem_Icc, tsub_le_iff_right] at hx ⊢
              constructor
              · suffices v.t₀ - v.r ≤ x by linarith
                exact le_trans t.2.1 hx.1.le
              · linarith [show 0 ≤ (v.r : ℝ) from v.r.2]
          set s: v.iccr := ⟨_, x_mem⟩  with hs
          rw[show x = ↑s by rfl]
          apply Real.le_iSup_of_bddAbove
            (f:=fun t : v.iccr => ‖v.b (↑t) (f.extended ↑t) - v.b (↑t) (g.extended ↑t)‖)
          --‖b(t,f(t)-b(t,g(t)‖ is bounded
          use 2 * v.M
          intro u ⟨t, ht⟩
          simp[← ht]
          calc ‖v.b t (f.extended t) - v.b t (g.extended t)‖
            _ ≤ ‖v.b t (f.extended t)‖ + ‖v.b t (g.extended t)‖ :=  norm_sub_le ..
            _ ≤ v.M +v.M := by gcongr <;> apply sub_norm_le
            _ = _ := by rw [two_mul]
        _ = |t - v.t₀| * ⨆ (t : v.iccr), ‖v.b t (f t) - v.b t (g t)‖ := by
          congr 1
          refine iSup_congr ?_
          rintro i
          simp only [extended_apply_of_mem]
        _ ≤ v.r * ⨆ (t : v.iccr), ‖v.b t (f t) - v.b t (g t)‖ := by
          apply mul_le_mul_of_nonneg_right
          · have := t.2
            rw [mem_iccr_iff] at this
            exact this
          · apply Real.iSup_nonneg
            intro _
            exact norm_nonneg _
        _ ≤ _ := by
          rw [FunSpace.dist_apply]
          erw [show v.r.1 * ⨆ t : v.iccr, ‖v.b t (f t) - v.b t (g t)‖ =
            ⨆ t : v.iccr, (v.r * ‖v.b (↑t) (f t) - v.b (↑t) (g t)‖) by
            rw [Real.mul_iSup_of_nonneg]
            · rfl
            -- refine le_antisymm ?_ ?_
              -- sorry
            · exact v.r.2]
          apply ciSup_le
          intro x

          have := v.isPL.lipschitz x (by
            have : v.iccr ⊆ Icc (v.t₀ - ↑v.α) (v.t₀ + ↑v.α) := by
              simp only [iccr]
              have : v.r.1 < v.α.1 := v.isPL.r_lt_α

              refine Icc_subset_Icc ?_ ?_
              · apply sub_le_sub_left
                exact le_of_lt this

              · apply add_le_add_left
                exact le_of_lt this
            exact this x.2) (x := f x) (y := g x) (by
            simp only [mem_setOf_eq]
            exact f.norm_le_β _) (by
            simp only [mem_setOf_eq]
            exact g.norm_le_β _)
          rw [edist_eq_coe_nnnorm_sub, edist_eq_coe_nnnorm_sub] at this
          norm_cast at this
          change (_ : ℝ) ≤ _ at this
          simp only [val_eq_coe, coe_nnnorm, NNReal.coe_mul] at this
          have : v.r * ‖v.b (x) (f x) - v.b (x) (g x)‖ ≤ v.r * ↑v.K * ‖f x - g x‖ := by
            rw [mul_assoc]
            apply mul_le_mul_of_nonneg_left
            · exact this
            · exact v.r.2
          refine this.trans ?_
          apply mul_le_mul
          · rw [mul_comm]
          · apply le_ciSup ?_ x
            obtain ⟨x, hx⟩ : BddAbove (range fun t ↦ ‖f t‖) := by exact bddAbove v f
            obtain ⟨y, hy⟩ : BddAbove (range fun t ↦ ‖g t‖) := by exact bddAbove v g
            use x + y
            rintro _ ⟨t, rfl⟩
            simp only
            specialize hx ⟨t, rfl⟩
            specialize hy ⟨t, rfl⟩
            simp only at hx hy
            refine le_trans (norm_sub_le ..) ?_
            gcongr
          · exact norm_nonneg (f x - g x)

          · apply mul_nonneg
            · exact v.K.2
            · exact v.r.2

    · exact extended_integrable ..
    · exact extended_integrable ..
  · obtain ⟨x, hx⟩ : BddAbove (range fun t ↦ ‖f.T t‖) := by exact bddAbove v f.T
    obtain ⟨y, hy⟩ : BddAbove (range fun t ↦ ‖g.T t‖) := by exact bddAbove v g.T
    use x + y
    rintro _ ⟨t, rfl⟩
    simp only
    specialize hx ⟨t, rfl⟩
    specialize hy ⟨t, rfl⟩
    simp only at hx hy

    -- simp? [upperBounds] at hx hy ⊢
    refine le_trans (norm_sub_le ..) ?_
    gcongr

/-- Prove that T is a contraction mapping: there exists a constant C = K * r with C < 1 such that for all f, g, we have
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
  · have := v.isPL.r_lt_K
    rw [lt_div_iff₀] at this

    . rwa [mul_comm]

    have := v.isPL.K_nezero
    exact pos_iff_ne_zero.mpr this
  rw [LipschitzWith]
  intro f g
  simp only [FunSpace.edist_apply, ENNReal.coe_mul]
  norm_cast
  change (_ : ℝ) ≤ _
  simp only [val_eq_coe, NNReal.coe_mul, coe_mk]
  apply dist_T
end FunSpace

/-- there exists a unique fixed point-/
theorem exists_unique_fixed : ∃! f : FunSpace v, f.T = f := by
  obtain ⟨K, hT⟩ := FunSpace.T_contract (E := E)
  -- `f` is a fixed point of the contraction map `T`
  let f : FunSpace v := ContractingWith.fixedPoint _ hT
  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⟩