AutoSamplingTheory.TechnicalLemmas.Analysis.GradientFlowLastIterate

- The source Lyapunov decreases along an actual convex gradient trajectory, yielding last-time gradient and improved objective upper bounds.

theorem lyapunov_and_rates {f : E → ℝ} {X : ℝ → E} {z : E} {T : ℝ}
    (hT : 0 ≤ T) (hf : ContDiff ℝ 2 f) (hc : ConvexOn ℝ univ f)
    (hz : IsMinOn f univ z) (hX : ContinuousOn X (Icc 0 T))
    (hflow : ∀ t ∈ Ico 0 T, HasDerivWithinAt X (-gradient f (X t)) (Ici t) t) :
    AntitoneOn (fun t => t ^ 2 * ‖gradient f (X t)‖ ^ 2 +
      2 * t * (f (X t) - f z) + ‖X t - z‖ ^ 2) (Icc 0 T) ∧
    ∀ t ∈ Ioc 0 T, ‖gradient f (X t)‖ ^ 2 ≤ ‖X 0 - z‖ ^ 2 / t ^ 2 ∧
      f (X t) - f z ≤ ‖X 0 - z‖ ^ 2 / (4 * t) := by
  have hdf : Differentiable ℝ f := hf.differentiable (by norm_num)
  have hsc : StrongConvexOn univ 0 f := strongConvexOn_zero.mpr hc
  have hH := (ConvexityC2.gradient_mono_iff_fderiv2_lower hf).mp (fun x y =>
    StrongConvexFirstOrder.gradient_inner_lower_bound_of_strongConvexOn hsc
      (fun w _ => (hdf w).hasGradientAt) (mem_univ x) (mem_univ y))
  let R : (E →L[ℝ] ℝ) →L[ℝ] E :=
    { toFun := (toDual ℝ E).symm
      map_add' := (toDual ℝ E).symm.map_add
      map_smul' := by intros; simp
      cont := (toDual ℝ E).symm.continuous }
  let H (x : E) : E →L[ℝ] E := R.comp (fderiv ℝ (fderiv ℝ f) x)
  have hfd : ContDiff ℝ 1 (fderiv ℝ f) := hf.fderiv_right (by norm_num)
  have hg (x : E) : HasFDerivAt (gradient f) (H x) x :=
    R.hasFDerivAt.comp x (hfd.differentiable_one x).hasFDerivAt
  have hpos (x v : E) : 0 ≤ inner ℝ (H x v) v := by
    have hi : inner ℝ (H x v) v = (fderiv ℝ (fderiv ℝ f) x v) v := toDual_symm_apply
    simpa only [hi, zero_mul] using hH x v
  have hsupp (x : E) : f x - f z ≤ inner ℝ (gradient f x) (x - z) := by
    have h := StrongConvexFirstOrder.firstOrder_lower_bound_of_strongConvexOn hsc
      (fun w _ => (hdf w).hasGradientAt) (mem_univ x) (mem_univ z)
    rw [show z - x = -(x - z) by abel, inner_neg_right] at h
    simp only [zero_div, zero_mul, add_zero] at h
    linarith
  let L : ℝ → ℝ := fun t => t ^ 2 * ‖gradient f (X t)‖ ^ 2 +
    2 * t * (f (X t) - f z) + ‖X t - z‖ ^ 2
  let D : ℝ → ℝ := fun t => -2 * t ^ 2 * inner ℝ (H (X t) (gradient f (X t)))
    (gradient f (X t)) + 2 * (f (X t) - f z) - 2 * inner ℝ (gradient f (X t)) (X t - z)
  have hcont : ContinuousOn L (Icc 0 T) :=
    ((continuousOn_id.pow 2).mul (((continuous_iff_continuousAt.mpr (fun x => (hg x).continuousAt)).comp_continuousOn hX).norm.pow 2)).add
      (((continuousOn_const.mul continuousOn_id).mul ((hf.continuous.comp_continuousOn hX).sub continuousOn_const))) |>.add
        ((hX.sub continuousOn_const).norm.pow 2)
  have hd (t : ℝ) (ht : t ∈ Ico 0 T) : HasDerivWithinAt L (D t) (Ici t) t := by
    have hn := ((hg (X t)).comp_hasDerivWithinAt t (hflow t ht)).norm_sq
    have he : HasDerivWithinAt (fun s => f (X s)) (-‖gradient f (X t)‖ ^ 2) (Ici t) t := by
      have h : HasFDerivAt f (toDual ℝ E (gradient f (X t))) (X t) := (hdf (X t)).hasGradientAt
      simpa only [Function.comp_def, toDual_apply_apply, inner_neg_right,
-- Source excerpt truncated; follow the exact source link.

AutoSamplingTheory/TechnicalLemmas/Analysis/GradientFlowLastIterate.lean:22published source at 0e31a3cda412Open detailed card

Excerpt truncated; the exact source link is authoritative.