import Mathlib.Order.LiminfLimsup
import Mathlib.Topology.Defs.Filter
import Mathlib.Data.Real.EReal
import Optlib.Differential.Calculation
import Optlib.Function.Proximal

noncomputable section

open Filter BigOperators Set Topology

variable {E : Type*}
variable [NormedAddCommGroup E] [InnerProductSpace ℝ E]
variable {f g : E → ℝ} {x y u v : E} {c : ℝ}

/- the general differential function used in the definition -/
def differential_fun (x : E) (f : E → ℝ) (u : E) :=
  fun y ↦ Real.toEReal ((f y - f x - inner u (y - x)) / ‖y - x‖)

/- the definition of the Frechet subdifferential-/
def f_subdifferential (f : E → ℝ) (x : E) : Set E :=
  {v : E | liminf (differential_fun x f v) (𝓝[≠] x) ≥ 0}

/- the definition of the limit subdifferential-/
def subdifferential (f : E → ℝ) (x : E) : Set E :=
  {v₀ : E | ∃ u : ℕ → E, Tendsto u atTop (𝓝 x) ∧ Tendsto (fun n ↦ f (u n)) atTop (𝓝 (f x))
    ∧ (∃ v : ℕ → E, ∀ n, v n ∈ f_subdifferential f (u n) ∧ Tendsto v atTop (𝓝 v₀))}

/- the domain of the function is the points whose subifferential are non empty -/
def active_domain (f : E → ℝ) : Set E :=
  {x | subdifferential f x ≠ ∅}

/- the critial point of a function -/
def critial_point (f : E → ℝ) : Set E :=
  {x | 0 ∈ subdifferential f x}

/-- equivalence of Frechet subdifferential -/
theorem has_f_subdiff_iff : u ∈ f_subdifferential f x ↔
    ∀ ε > 0, ∀ᶠ y in 𝓝 x, f y - f x - inner u (y - x) ≥ -ε * ‖y - x‖ := by
  have h0 : (∀ ε > 0, ∀ᶠ y in 𝓝[≠] x, f y - f x - inner u (y - x) > -ε * ‖y - x‖)
      ↔ ∀ ε > 0, ∀ᶠ y in 𝓝 x, f y - f x - inner u (y - x) ≥ -ε * ‖y - x‖ := by
    constructor
    · intro h ε εpos
      specialize h ε εpos
      rw [eventually_nhdsWithin_iff] at h
      filter_upwards [h] with y hy
      by_cases heq : y = x; rw [heq]; simp
      exact le_of_lt (hy heq)
    · intro h ε εpos
      specialize h (ε / 2) (by positivity)
      rw [eventually_nhdsWithin_iff]
      filter_upwards [h] with y h hy
      have : 0 < ε * ‖y - x‖ := mul_pos εpos (norm_sub_pos_iff.2 hy)
      linarith
  rw [← h0]
  simp only [f_subdifferential, mem_setOf_eq, liminf, limsInf, eventually_map]
  let sa := {a | ∀ᶠ (y : E) in 𝓝[≠] x, a ≤ differential_fun x f u y}
  constructor
  · intro (h : 0 ≤ sSup sa) ε εpos
    have hn : sa.Nonempty := by
      by_contra hn
      have : sa = ∅ := not_nonempty_iff_eq_empty.mp hn
      rw [this, sSup_empty] at h
      absurd h; exact of_decide_eq_false rfl
    have hsa : Real.toEReal (-ε) < sSup sa := by
      apply lt_of_lt_of_le _ h
      rw [EReal.coe_neg']
      exact neg_neg_iff_pos.mpr εpos
    obtain ⟨a, as, ha⟩ := exists_lt_of_lt_csSup hn hsa
    rw [mem_setOf_eq] at as
    apply Eventually.mp as
    apply eventually_nhdsWithin_of_forall
    rintro y hy h
    have := (lt_div_iff₀ (norm_sub_pos_iff.2 hy)).1 (EReal.coe_lt_coe_iff.1 (lt_of_lt_of_le ha h))
    linarith
  · intro h
    show 0 ≤ sSup sa
    rw [le_sSup_iff]
    intro b hb
    rw [mem_upperBounds] at hb
    contrapose! hb
    have h' : ∀ ε > 0, ∀ᶠ (y : E) in 𝓝[≠] x, differential_fun x f u y > -ε := by
      intro ε εpos
      by_cases hε : ε = ⊤
      · filter_upwards with a
        rw [hε]
        exact Batteries.compareOfLessAndEq_eq_lt.mp rfl
      have heq : ε.toReal = ε := EReal.coe_toReal hε (LT.lt.ne_bot εpos)
      have : 0 < ε.toReal := by
        rw [← EReal.coe_lt_coe_iff]
        exact lt_of_lt_of_eq εpos (id (Eq.symm heq))
      specialize h ε.toReal this
      apply Eventually.mp h
      apply eventually_nhdsWithin_of_forall
      rintro y hy h
      rw [← heq, ← EReal.coe_neg, differential_fun, gt_iff_lt, EReal.coe_lt_coe_iff]
      rw [lt_div_iff₀ (norm_sub_pos_iff.2 hy)]
      linarith
    by_cases hnb : b = ⊥
    · use -1
      constructor
      · specialize h' 1 (zero_lt_one' EReal)
        filter_upwards [h'] with y
        exact le_of_lt
      · rw [hnb]
        exact Batteries.compareOfLessAndEq_eq_lt.mp rfl
    · use b / 2
      have heq : b.toReal = b := EReal.coe_toReal (LT.lt.ne_top hb) hnb
      change b < Real.toEReal 0 at hb
      rw [← heq, EReal.coe_lt_coe_iff] at hb
      constructor
      · have : Real.toEReal 0 < -(b / Real.toEReal 2) := by
          rw [← heq, ← EReal.coe_div, ← EReal.coe_neg, EReal.coe_lt_coe_iff]
          linarith
        specialize h' (-(b / 2)) this
        simp only [neg_neg] at h'
        rw [mem_setOf]
        filter_upwards [h'] with y
        exact le_of_lt
      · show b < b / Real.toEReal 2
        rw [← heq, ← EReal.coe_div, EReal.coe_lt_coe_iff]
        linarith

/-- frechet subdifferential is a subset of limit subdifferential -/
theorem subdifferential_subset (f : E → ℝ) (x : E): f_subdifferential f x ⊆ subdifferential f x :=
  fun v vin ↦ ⟨(fun _ ↦ x), tendsto_const_nhds, tendsto_const_nhds,
  ⟨fun _ ↦ v, fun _ ↦ ⟨vin, tendsto_const_nhds⟩⟩⟩

/-- if f is a convex function, Frechet subdifferential is equal to subgradient-/
theorem convex_f_f_subdiff_eq_subgradient (f : E → ℝ) (x : E)
    (hconv : ConvexOn ℝ univ f) : f_subdifferential f x = SubderivAt f x := by
  rw [SubderivAt]
  ext g
  rw[mem_setOf, HasSubgradientAt]
  constructor
  · intro hg
    by_contra h'
    push_neg at h'
    rcases h' with ⟨y', hy'⟩
    rw[has_f_subdiff_iff] at hg
    rw[ConvexOn] at hconv
    rcases hconv with ⟨convset,convfun⟩
    have xin: x ∈ univ:= by
      simp
    have yin': y' ∈ univ:= by
      simp
    specialize convfun xin yin'
    have pos: 0 < (1 / 2) * ((f x) + inner g (y' - x) - f y') / ‖y' - x‖:=by
      apply div_pos
      · apply mul_pos
        simp; simp
        apply hy'
      · apply norm_pos_iff.mpr
        by_contra yeq'
        rw [sub_eq_zero] at yeq'
        rw [yeq'] at hy'
        simp at hy'
    rw[← gt_iff_lt] at pos
    specialize hg ((1 / 2) * ((f x) + inner g (y' - x) - f y')/‖y' - x‖)
    specialize hg pos
    simp at hg
    rw[Filter.Eventually,mem_nhds_iff] at hg
    rcases hg with ⟨T,tin,topen,xint⟩
    let S:= {x_1 | ∃(r : ℝ), 0 < r  ∧  r < 1 ∧ x_1 = r • x + (1 -r) • y'}
    let ST:= S ∩ T
    have STnonempty: ∃ x_1, x_1 ∈ ST:=by
      rw [Metric.isOpen_iff] at topen
      specialize topen x xint
      rcases topen with ⟨δ, posδ,hδ⟩
      let δ':= min δ ‖y' - x‖
      let δ'' := 1 - (1 / 2) * (δ' / ‖y' - x‖)
      use (δ'') • x + (1 - δ'') • y'
      apply mem_inter
      · rw[mem_setOf]
        use δ''
        constructor
        · apply sub_pos_of_lt
          simp
          refine (inv_mul_lt_iff₀ ?h.left.a.h).mpr ?h.left.a.a
          · simp
          · simp
            apply lt_of_le_of_lt
            apply (div_le_one _).mpr
            apply min_le_right
            apply norm_pos_iff.mpr
            by_contra yeq'
            rw[sub_eq_zero] at yeq'
            rw[yeq'] at hy'
            rw[sub_self, inner_zero_right,add_zero, lt_iff_not_le] at hy'
            apply hy'
            simp
            simp
        constructor
        · change 1 - 1 / 2 * (δ' / ‖y' - x‖) < 1
          simp
          apply div_pos
          · apply lt_min
            apply posδ
            apply norm_pos_iff.mpr
            by_contra yeq'
            rw[sub_eq_zero] at yeq'
            rw[yeq'] at hy'
            rw[sub_self, inner_zero_right,add_zero, lt_iff_not_le] at hy'
            apply hy'
            simp
          · apply norm_pos_iff.mpr
            by_contra yeq'
            rw[sub_eq_zero] at yeq'
            rw[yeq'] at hy'
            rw[sub_self, inner_zero_right,add_zero, lt_iff_not_le] at hy'
            apply hy'
            simp
        simp
      apply mem_of_subset_of_mem hδ
      rw[Metric.ball, mem_setOf,dist_eq_norm]
      have this: δ'' • x + (1 - δ'') • y' - x = (1 - δ'') • (y' - x):=by
        rw[smul_sub,sub_smul 1 δ'',sub_smul 1 δ'']
        rw[add_sub, sub_sub_sub_eq, add_comm (1 • y'), one_smul, one_smul]
        rw[sub_sub]
      rw[this, norm_smul]
      simp
      rw[← sub_add]; simp
      rw[abs_eq_self.mpr]
      rw[mul_assoc]
      have this: δ' / ‖y' - x‖ * ‖y' - x‖ = δ':=by
        have nonzero: ‖y' - x‖ ≠ 0:=by
          by_contra yeq'
          rw[norm_eq_zero,sub_eq_zero] at yeq'
          rw[yeq'] at hy'
          rw[sub_self, inner_zero_right,add_zero, lt_iff_not_le] at hy'
          apply hy'
          simp
        refine div_mul_cancel₀ δ' nonzero
      rw[this]
      refine (inv_mul_lt_iff₀ ?h.hb.h).mpr ?h.hb.a
      simp
      apply lt_of_le_of_lt
      apply min_le_left
      exact lt_two_mul_self posδ
      simp
      apply div_nonneg
      apply le_min
      linarith
      apply norm_nonneg
      apply norm_nonneg
    rcases STnonempty with ⟨x1,hx1⟩
    rw[mem_inter_iff] at hx1
    rcases hx1 with ⟨x1s,x1t⟩
    rw[mem_setOf] at x1s
    rcases x1s with ⟨r,rpos,rltone,x1eq⟩
    have x1in: x1 ∈ {x_1 | inner g (x_1 - x) ≤
        f x_1 - f x + 2⁻¹ * (f x + inner g (y' - x) - f y') / ‖y' - x‖ * ‖x_1 - x‖}:=by
      apply mem_of_subset_of_mem tin
      assumption
    rw[mem_setOf,x1eq] at x1in
    rw[add_comm] at x1in
    have this: (1 - r) • y' + r • x - x = (1 - r) • (y' - x):=by
      rw[smul_sub,sub_smul 1 r,sub_smul 1 r]
      rw[sub_sub_sub_eq, add_comm (1 • y'), one_smul, one_smul,add_comm]
      rw[add_sub_add_comm, add_sub,add_sub]
      simp
      rw[add_comm, add_comm (r • x - r • y'),add_sub]
    rw[this] at x1in
    rw[inner_smul_right, norm_smul] at x1in
    have rnonneg: 0 ≤ r:=by linarith
    have rleone: 0 ≤ 1-r:=by linarith
    have r2pos: 0 < (1 -r)/2:=by linarith
    have req: r + (1-r) = 1:=by simp
    specialize convfun rnonneg rleone req
    have nonneg: 0 ≤ f y' - f x - inner g (y' - x):=by
      apply nonneg_of_mul_nonneg_right _ r2pos
      rw[mul_sub, ← sub_self_div_two (1 - r), sub_mul, sub_mul (1 - r)]
      simp
      apply le_trans x1in
      rw[add_comm ((1 - r) • y'), sub_add, sub_le_iff_le_add]
      apply le_trans convfun
      simp;
      rw[abs_eq_self.mpr rleone]
      rw[← mul_assoc]; rw[← sub_le_iff_le_add]
      rw[← sub_add, add_comm (r*f x), add_comm (f x), ← add_sub, ← add_sub, mul_add]
      nth_rw 2 [← one_mul (f x)]
      rw[← sub_mul]
      nth_rw 2 [ ← neg_sub ]
      rw[neg_mul,← sub_eq_add_neg ((1 - r) * f y'),← mul_sub, mul_assoc, mul_comm (1 - r) ‖y' - x‖]
      rw[← mul_assoc, div_mul, div_self]
      simp
      rw[mul_comm (2⁻¹ * inner g (y' - x) + 2⁻¹ * (f x - f y')),
        mul_add, add_comm ((1 - r) * (2⁻¹ * inner g (y' - x)))]
      rw[← add_assoc, ← mul_assoc, ← mul_assoc,inv_eq_one_div]
      linarith
      by_contra yeq'
      rw[norm_eq_zero,sub_eq_zero] at yeq'
      rw[yeq'] at hy'
      rw[sub_self, inner_zero_right,add_zero, lt_iff_not_le] at hy'
      apply hy'
      simp
    have nonneg': ¬ 0 > f y' - f x - inner g (y' - x):=by linarith
    apply nonneg'
    simp
    linarith
  · intro h
    rw[has_f_subdiff_iff]
    intro ε εpos
    filter_upwards
    intro y
    rw[ge_iff_le]
    apply le_trans
    simp
    apply neg_le.mpr
    have pos: - 0 ≤ ε * ‖y - x‖:=by
      simp
      rw[mul_comm]
      apply (mul_nonneg_iff_left_nonneg_of_pos εpos).mpr
      simp
    apply pos
    simp
    specialize h y
    simp at h
    linarith

/-- correlation of the Frechet subdifferential between negative function -/
theorem f_subdiff_neg_f_subdiff_unique (hu : u ∈ f_subdifferential f x)
    (hv : v ∈ f_subdifferential (- f) x) : u = - v := by
  rw [has_f_subdiff_iff] at *
  have h : ∀ ε > 0, ∀ᶠ y in 𝓝 x, inner (u + v) (y - x) ≤ ε * ‖y - x‖ := by
    intro ε εpos
    have ε2pos : 0 < ε / 2 := by positivity
    filter_upwards [hu _ ε2pos, hv _ ε2pos] with y huy hvy
    rw [InnerProductSpace.add_left]
    simp only [Pi.neg_apply, sub_neg_eq_add] at hvy
    linarith
  by_cases heq : u + v = 0; exact eq_neg_of_add_eq_zero_left heq
  apply eq_of_forall_dist_le
  rw [dist_eq_norm, sub_neg_eq_add]
  intro ε εpos
  specialize h ε εpos
  rw [Metric.eventually_nhds_iff_ball] at h
  obtain ⟨δ, δpos, hd⟩ := h
  have hne := norm_ne_zero_iff.mpr heq
  have hb : x + (δ / 2 / ‖u + v‖) • (u + v) ∈ Metric.ball x δ := by
    rw [mem_ball_iff_norm', sub_add_cancel_left]
    rw [norm_neg, norm_smul, Real.norm_eq_abs, abs_div, abs_norm]
    rw [div_mul_cancel₀ _ hne, abs_of_nonneg (by positivity)]
    linarith
  specialize hd (x + ((δ / 2) / ‖u + v‖) • (u + v)) hb
  rw [add_sub_cancel_left, inner_smul_right, norm_smul, Real.norm_eq_abs, abs_div, abs_norm] at hd
  rw [real_inner_self_eq_norm_mul_norm, ← mul_assoc, div_mul_cancel₀ _ hne] at hd
  rw [div_mul_cancel₀ _ hne, abs_of_nonneg (by positivity), mul_comm] at hd
  exact le_of_mul_le_mul_right hd (by positivity)

/-- the calculation rule for addition -/
theorem f_subdiff_add (hf : u ∈ f_subdifferential f x) (hg : v ∈ f_subdifferential g x) :
    u + v ∈ f_subdifferential (f + g) x := by
  rw [has_f_subdiff_iff] at *
  intro ε εpos
  have ε2pos : 0 < ε / 2 := by positivity
  filter_upwards [hf _ ε2pos, hg _ ε2pos] with y hfy hgy
  simp only [Pi.add_apply, neg_mul, ge_iff_le, neg_le_sub_iff_le_add]
  rw [InnerProductSpace.add_left]
  linarith

/-- the calculation rule for functions timing a positive constant -/
theorem f_subdiff_smul (h : u ∈ f_subdifferential (c • f) x) (cpos : 0 < c) :
    c⁻¹ • u ∈ f_subdifferential f x := by
  rw [has_f_subdiff_iff] at *
  intro ε εpos
  filter_upwards [h _ (mul_pos cpos εpos)] with y hy
  rw [real_inner_smul_left]
  simp only [Pi.smul_apply, smul_eq_mul, neg_mul, neg_le_sub_iff_le_add] at hy
  apply (mul_le_mul_left cpos).mp
  field_simp
  linarith

/-- first order optimality condition for unconstrained optimization problem -/
theorem first_order_optimality_condition (f : E → ℝ) (x₀ : E) (hx : IsLocalMin f x₀) :
    (0 : E) ∈ f_subdifferential f x₀ := by
  rw [has_f_subdiff_iff]
  intro ε εpos
  filter_upwards [hx] with y hy
  have : 0 ≤ ε * ‖y - x₀‖ := by positivity
  simp only [inner_zero_left, sub_zero, neg_mul, ge_iff_le, neg_le_sub_iff_le_add]
  linarith

/-- first order optimality condition for unconstrained optimization problem -/
theorem first_order_optimality_condition' (f : E → ℝ) (x₀ : E) (hx: IsLocalMin f x₀) :
    (0 : E) ∈ subdifferential f x₀ := by
  obtain hcon := subdifferential_subset f x₀
  apply hcon; exact first_order_optimality_condition f x₀ hx

end

section

open Filter BigOperators Set Topology

variable {E : Type*}
variable [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
variable {f g : E → ℝ} {x y u v : E} {c : ℝ}

/--an equal statement for differential function in Frechet subdifferential-/
theorem HasGradientAt_iff_f_subdiff :
    HasGradientAt f u x ↔ u ∈ f_subdifferential f x ∧ -u ∈ f_subdifferential (-f) x := by
  rw [hasGradientAt_iff_isLittleO, Asymptotics.isLittleO_iff]
  rw [has_f_subdiff_iff, has_f_subdiff_iff]
  constructor
  · intro h
    constructor
    · intro ε εpos
      filter_upwards [h εpos] with y hy
      rw [Real.norm_eq_abs, abs_le] at hy
      linarith
    · intro ε εpos
      filter_upwards [h εpos] with y hy
      rw [Real.norm_eq_abs, abs_le] at hy
      simp only [Pi.neg_apply, sub_neg_eq_add, inner_neg_left, neg_mul]
      linarith
  · intro ⟨h1, h2⟩ c cpos
    filter_upwards [h1 c cpos, h2 c cpos] with y h1y h2y
    simp only [Pi.neg_apply, sub_neg_eq_add, inner_neg_left, neg_mul] at h2y
    rw [Real.norm_eq_abs, abs_le]
    constructor <;> linarith

/-- the Frechet subdifferential of a differentiable function is its gradient set-/
theorem f_subdiff_gradiant (f : E → ℝ) (f': E → E) (z : E)(hf : HasGradientAt f (f' z) z) :
    f_subdifferential f z = {f' z} := by
  ext u
  rw [mem_singleton_iff]
  rw [HasGradientAt_iff_f_subdiff] at hf
  constructor
  · exact fun h ↦(neg_neg (f' z)) ▸ (f_subdiff_neg_f_subdiff_unique h hf.2)
  · exact fun h ↦ h ▸ hf.1

/-- the subdifferential of a differentiable function is its gradient set-/
theorem subdiff_gradient (f : E → ℝ) (f': E → E) (hf : ∀ x₁, HasGradientAt f (f' x₁) x₁)
    (gradcon: Continuous f') (z : E) : subdifferential f z = {f' z} := by
  rw [subdifferential]
  ext x
  constructor
  · intro xin
    rw [mem_setOf] at *
    rcases xin with ⟨u, ⟨utendz, ⟨utendfz, ⟨v, hv⟩⟩⟩⟩
    have veq : ∀ (n : ℕ), v n = f' (u n) := by
      intro n
      rcases hv n with ⟨vin,vtend⟩
      rw [f_subdiff_gradiant f f' ] at vin
      exact vin
      exact hf (u n)
    apply tendsto_nhds_unique (hv 1).right
    rw[tendsto_congr veq]
    apply tendsto_atTop_nhds.mpr
    intro U uin uopen
    rw[continuous_def] at gradcon
    rw[tendsto_atTop_nhds] at utendz
    have zinvu : z ∈ ((f') ⁻¹' U) := by simp; assumption
    rcases utendz ((f') ⁻¹' U) zinvu (gradcon U uopen) with ⟨N, hN⟩
    use N
    intro n nge
    change u n ∈ (f') ⁻¹' U
    apply hN n nge
  · intro xin
    rw [mem_setOf,xin]
    use fun _ ↦ z
    constructor; simp
    constructor; simp
    use fun _ ↦ f' z
    intro _ ;constructor;
    rw [f_subdiff_gradiant f f']
    rfl
    apply hf z
    simp only [tendsto_const_nhds_iff]

theorem f_subdiff_add_smooth (h : u ∈ f_subdifferential f x) (hg : HasGradientAt g v x) :
    u + v ∈ f_subdifferential (f + g) x :=
  f_subdiff_add h (HasGradientAt_iff_f_subdiff.mp hg).1

lemma f_subdiff_prox (h : prox_prop f y x) : y - x ∈ f_subdifferential f x := by
  have : IsLocalMin (fun u ↦ f u + ‖u - y‖ ^ 2 / 2) x := by
    have := h.localize
    rwa [IsLocalMinOn, nhdsWithin_univ] at this
  have hd := first_order_optimality_condition _ _ this
  have hg :=  HasGradientAt.neg (@gradient_of_sq _ _ _ _ y x)
  have := f_subdiff_add_smooth hd hg
  simp only [neg_sub, zero_add] at this
  have hf : f = (fun u ↦ f u + ‖u - y‖ ^ 2 / 2) + fun x ↦ -(‖x - y‖ ^ 2 / 2) := by
    ext x
    simp only [Pi.add_apply, add_neg_cancel_right]
  exact hf ▸ this

/--if one function is differentiable, the Frechet subdifferential of the sum of two functions
can be transverted to the sum of Frechet subdifferential for each function-/
theorem f_subdiff_add' (f : E → ℝ ) (g : E → ℝ ) (g' : E → E) (x : E)
    (hg : ∀ x₁, HasGradientAt g (g' x₁) x₁) (z : E):
    z ∈ f_subdifferential (f + g) x ↔ ∃ zf ∈ f_subdifferential f x , ∃ zg ∈ f_subdifferential g x ,
    z = zf + zg := by
  constructor
  · intro zin
    use z - g' x
    constructor
    · rw[has_f_subdiff_iff] at *
      intro ε εpos
      specialize hg x
      rw[hasGradientAt_iff_isLittleO, Asymptotics.isLittleO_iff] at hg
      have ε2pos : 0 < ε / 2 := by positivity
      specialize hg ε2pos
      filter_upwards [zin _ ε2pos, hg ] with a za ga
      simp at ga
      have h: - (g a - g x - inner (g' x) (a - x)) ≥ -(ε / 2) * ‖a - x‖:=by
        change -(ε / 2) * ‖a - x‖ ≤ - (g a - g x - inner (g' x) (a - x))
        rw[neg_mul, neg_le_neg_iff]
        apply le_trans; apply le_abs_self; assumption
      rw[inner_sub_left];
      simp; simp at h za
      linarith
    · use g' x
      constructor
      · rw[f_subdiff_gradiant g g']
        simp
        exact hg x
      · simp
  · intro zin
    rcases zin with ⟨zf,zfin,zg,zgin,fgadd⟩
    rw[fgadd]
    apply f_subdiff_add;
    repeat' assumption

/--if one function is smooth, the subdifferential of the sum of two functions
can be transverted to the sum of subdifferential for each function-/
theorem subdiff_add (f : E → ℝ) (g : E → ℝ) (g' : E → E) (x : E)
    (hg : ∀ x₁, HasGradientAt g (g' x₁) x₁) (gcon : Continuous g)
      (gradcon : Continuous g') (z : E):
        z ∈ subdifferential (f + g) x ↔ ∃ zf ∈ subdifferential f x,
          ∃ zg ∈ subdifferential g x, z = zf + zg := by
  constructor
  · intro zin
    rw[subdifferential,mem_setOf] at zin
    rcases zin with ⟨u,hux,hufx,hv⟩
    rcases hv with ⟨v,vlim⟩
    use z - g' x
    constructor
    · rw[subdifferential,mem_setOf]
      constructor
      · constructor
        use hux
        constructor
        · have glim: Tendsto (fun n ↦ -g (u n)) atTop (𝓝 (-g x)):=by
            have contneg: Continuous (-g):=by
              exact continuous_neg_iff.mpr gcon
            apply tendsto_atTop_nhds.mpr
            intro U uin uopen
            rw[continuous_def] at contneg
            rw[tendsto_atTop_nhds] at hux
            have invuopen:IsOpen ((-g) ⁻¹' U):=by
              exact contneg U uopen
            have xinvu: x ∈ ((-g) ⁻¹' U):=by
              simp;exact uin
            rcases hux ((-g) ⁻¹' U) xinvu invuopen with ⟨N,hN ⟩
            use N
            intro n nge
            change u n ∈ (-g) ⁻¹' U
            apply hN n nge
          have functrans: (fun n ↦ f (u n)) = (fun n ↦ ((f+g) (u n)) + (-g (u n))):=by
            ext n
            simp
          rw[functrans]
          have nhds_trans: 𝓝 (f x) = (𝓝 ((f + g) x + -g x)):=by
            simp
          rw[nhds_trans]
          apply Filter.Tendsto.add hufx glim
        use fun n ↦ (v n) - (g' (u n))
        intro n
        rcases vlim n with ⟨vin,vtends⟩
        constructor
        rw[f_subdiff_add'] at vin
        rw[f_subdiff_gradiant g g'] at vin
        rcases vin with ⟨zf,zfin,zg,zgin,fgadd⟩
        simp at zgin; simp
        rw [fgadd, zgin]
        simp; assumption
        exact hg (u n)
        use g';exact hg
        have gradlim: Tendsto (fun n ↦   g' (u n)) atTop (𝓝 (  g' x)):=by
          apply tendsto_atTop_nhds.mpr
          intro U uin uopen
          rw[continuous_def] at gradcon
          rw[tendsto_atTop_nhds] at hux
          have invuopen:IsOpen ((g') ⁻¹' U):=by
              exact gradcon U uopen
          have xinvu: x ∈ ((g') ⁻¹' U):=by
              simp;exact uin
          rcases hux ((g') ⁻¹' U) xinvu invuopen with ⟨N,hN ⟩
          use N
          intro n nge
          change u n ∈ (g') ⁻¹' U
          apply hN n nge
        apply Tendsto.sub vtends
        assumption

    · use g' x
      constructor
      · rw[subdiff_gradient g g' hg gradcon]
        simp
      · simp

  · intro zin
    rcases zin with ⟨zf,zfin,zg,zgin,fgadd⟩
    rw[fgadd,subdifferential,mem_setOf]
    rw[subdifferential,mem_setOf] at zfin zgin
    rcases zfin with ⟨uf,ufx,uffx,hfv⟩
    rcases hfv with ⟨vf,vflim⟩
    rcases zgin with ⟨ug,ugx,uggx,hgv⟩
    rcases hgv with ⟨vg,vglim⟩
    constructor
    constructor
    use ufx
    constructor
    · apply Filter.Tendsto.add
      exact uffx
      apply tendsto_atTop_nhds.mpr
      intro U uin uopen
      rw[continuous_def] at gcon
      rw[tendsto_atTop_nhds] at ufx
      have invuopen:IsOpen ((g) ⁻¹' U):=by
        exact gcon U uopen
      have xinvu: x ∈ ((g) ⁻¹' U):=by
        simp; exact uin
      rcases ufx ((g) ⁻¹' U) xinvu invuopen with ⟨N,hN ⟩
      use N
      intro n nge
      change uf n ∈ (g) ⁻¹' U
      apply hN n nge
    · use fun n ↦ (vf n) + g' (uf n)
      intro n
      constructor
      rcases vglim n with ⟨vgin,vgtends⟩
      rcases vflim n with ⟨vfin,vftends⟩
      · rw[f_subdiff_add' f g g']
        rw[f_subdiff_gradiant g g'];
        rw[f_subdiff_gradiant g g'] at vgin; simp at vgin
        use vf n
        constructor
        assumption
        use g' (uf n)
        constructor
        simp ;simp;
        apply hg (ug n)
        apply hg (uf n)
        repeat' assumption;
      · apply Filter.Tendsto.add
        rcases vflim n with ⟨_,vflim⟩
        apply vflim
        have limgrad: (An: ℕ → E) → (x : E) → (Tendsto An atTop (𝓝 x))→ Tendsto (fun n ↦ g' (An n))
            atTop (𝓝 (g' x)):=by
          intro An x antends
          apply tendsto_atTop_nhds.mpr
          intro U uin uopen
          rw[continuous_def] at gradcon
          rw[tendsto_atTop_nhds] at antends
          have invuopen:IsOpen ((g') ⁻¹' U):=by
              exact gradcon U uopen
          have xinvu: x ∈ ((g') ⁻¹' U):=by
              simp;exact uin
          rcases antends ((g') ⁻¹' U) xinvu invuopen with ⟨N,hN ⟩
          use N
          intro n nge
          change An n ∈ (g') ⁻¹' U
          apply hN n nge
        rcases vglim n with ⟨vgin,vgtends⟩
        rw[f_subdiff_gradiant g g'] at vgin
        have funtrans: ∀ (n : ℕ ),  vg n = g' (ug n):=by
          intro k; rcases vglim k with ⟨vgin',vgtends'⟩;
          rw[f_subdiff_gradiant g g'] at vgin'
          repeat' assumption
          apply hg (ug k)
        rw[tendsto_congr funtrans] at vgtends
        have zgeq: zg = g' x:=by
          apply tendsto_nhds_unique vgtends
          apply limgrad ;apply ugx
        rw[zgeq]
        apply limgrad ; apply ufx;
        apply hg (ug n)

lemma f_subdiff_smul_prox (h : prox_prop (c • f) u x) (cpos : 0 < c) :
    c⁻¹ • (u - x) ∈ f_subdifferential f x := f_subdiff_smul (f_subdiff_prox h) cpos

/--the relation between subdifferential and poximal set-/
theorem rela_proximal_operator_partial (f : E → ℝ )(x : E)(u : E) :
    u ∈ prox_set f x → (x - u) ∈ subdifferential f u:=by
  intro uporx
  rw [prox_set, mem_setOf, prox_prop] at uporx
  have h: (0 : E) ∈ subdifferential (fun u ↦ f u + ‖u - x‖ ^ 2 / 2) u:=by
    apply mem_of_mem_of_subset
    apply first_order_optimality_condition'
    · apply IsMinOn.isLocalMin
      apply uporx; simp
    rfl
  have ngradient : ∀ x₁, HasGradientAt (fun u ↦  ‖u - x‖ ^ 2 / 2) (x₁ - x) x₁ := by
    intro x₁; exact gradient_of_sq x₁
  have _ncovex: ConvexOn ℝ Set.univ (fun u ↦  ‖u - x‖ ^ 2 / 2):=by
    apply convex_of_norm_sq x; exact convex_univ
  have ncon: Continuous (fun u ↦  ‖u - x‖ ^ 2 / 2):=by
    have funtrans:(fun u ↦  ‖u - x‖ ^ 2 / 2) = (fun u ↦  (1/2)*‖u - x‖ ^ 2):=by
      simp
      ext y; rw [mul_comm, div_eq_mul_inv]
    rw[funtrans]
    apply Continuous.mul
    simp
    exact continuous_const
    apply Continuous.pow
    apply Continuous.norm
    exact continuous_sub_right x
  have gradcon: Continuous fun u ↦ u-x:=by exact continuous_sub_right x
  obtain h' := (subdiff_add f (fun u ↦ ‖u - x‖ ^ 2 / 2) (fun x₁ ↦ x₁ - x)
    u ngradient ncon gradcon 0).mp h
  rcases h' with ⟨zf,zfin,zg,zgin,gfadd⟩
  have nsubdifference : subdifferential (fun u ↦ ‖u - x‖ ^ 2 / 2) u = {y|y = u - x}:=by
    exact subdiff_gradient (fun u ↦ ‖u - x‖ ^ 2 / 2) (fun u ↦ u - x) ngradient gradcon u
  rw [nsubdifference,mem_setOf] at zgin
  rw [zgin] at gfadd
  have zfeq : zf = - (u - x):=by
    apply add_eq_zero_iff_eq_neg.mp
    apply gfadd.symm
  rw [zfeq] at zfin
  simp at zfin
  assumption
