Gradient flow

Let z be the supplied global minimizer of f. Surjectivity gives xstar with g(xstar)=z. Every g(x) lies in the objective space, so f(g(xstar))=f(z)<=f(g(x)); thus the same xstar minimizes the composite. At y=g(x), the shared first-order strong-convexity bound at comparator z gives the gap at most <grad f(y),y-z> minus alpha times the squared distance divided by2. Cauchy-Schwarz bounds the inner product. The nonnegative square (norm grad f(y)−alpha norm(y−z))² yields the numerical PL bound for f. Put A_x=Dg(x). The Frechet chain rule gives D(f∘g)(x)[v]=<grad f(g(x)),A_x v>. The defining adjoint identity rewrites this as <A_x-adjoint grad f(g(x)),v>. Uniqueness of the Riesz representative identifies the actual composite gradient. Apply the assumed operator lower bound to v=grad f(g(x)). Its quadratic form equals norm(A_x-adjoint v)² by the adjoint identity. Multiply the base gradient-gap bound by nonnegative sigma and combine. Finally use g(xstar)=z to express the same gap relative to the attained composite minimum.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem exists_minimizer_and_pl {f : F → ℝ} {g : E → F} {α σ : ℝ} {z : F}
    (hα : 0 < α) (hσ : 0 ≤ σ) (hsc : StrongConvexOn univ α f)
    (hf : Differentiable ℝ f) (hg : Differentiable ℝ g)
    (hsurj : Function.Surjective g) (hz : IsMinOn f univ z)
    (hjac : ∀ x v, σ * ‖v‖ ^ 2 ≤
      inner ℝ v ((fderiv ℝ g x) ((fderiv ℝ g x).adjoint v))) :
    ∃ xstar, g xstar = z ∧ IsMinOn (f ∘ g) univ xstar ∧
      ∀ x, 2 * (α * σ) * ((f ∘ g) x - (f ∘ g) xstar) ≤
        ‖gradient (f ∘ g) x‖ ^ 2 := by
  obtain ⟨xstar, hxstar⟩ := hsurj z
  refine ⟨xstar, hxstar, ?_, ?_⟩
  · intro x _
    simpa [Function.comp_def, hxstar] using hz (mem_univ (g x))
  · intro x
    have hfirst := StrongConvexFirstOrder.firstOrder_lower_bound_of_strongConvexOn
      hsc (fun y _ => (hf y).hasGradientAt) (mem_univ (g x)) (mem_univ z)
    have hcs := real_inner_le_norm (gradient f (g x)) (g x - z)
    have hbase : 2 * α * (f (g x) - f z) ≤ ‖gradient f (g x)‖ ^ 2 := by
      rw [← neg_sub (g x) z, inner_neg_right, norm_neg] at hfirst
      nlinarith [sq_nonneg (‖gradient f (g x)‖ - α * ‖g x - z‖)]
    have hchain : HasGradientAt (f ∘ g)
        ((fderiv ℝ g x).adjoint (gradient f (g x))) x := by
      apply hasGradientAt_iff_hasFDerivAt.mpr
      have hc := (hf (g x)).hasGradientAt.hasFDerivAt.comp x (hg x).hasFDerivAt
      have heq : (InnerProductSpace.toDual ℝ F (gradient f (g x))).comp (fderiv ℝ g x) =
          InnerProductSpace.toDual ℝ E ((fderiv ℝ g x).adjoint (gradient f (g x))) := by
        ext v
        simp [InnerProductSpace.toDual_apply_apply, ContinuousLinearMap.adjoint_inner_left]
      rw [heq] at hc
      exact hc
    have hcoerc := hjac x (gradient f (g x))
    rw [← ContinuousLinearMap.adjoint_inner_left, real_inner_self_eq_norm_sq] at hcoerc
    have hmul := mul_le_mul_of_nonneg_left hbase hσ
    rw [hchain.gradient]
    dsimp only [Function.comp_def]
    rw [hxstar]
    nlinarith

end AutoSamplingTheory.TechnicalLemmas.Analysis.StrongConvexPLPullback

Exact module and namespace context

Frechet differentiability represents Df(X(t)) by its Riesz gradient. Compose this derivative with the supplied right derivative X prime(t)=-gradient f(X(t)). The inner product of the gradient with its negative is minus its squared norm. This constructs the energy identity from the actual dynamics. Let e(t)=f(X(t))-f(z). Subtracting the constant minimum preserves the derivative. PL gives 2 alpha e(t)<=norm gradient f(X(t)) squared, hence the actual right derivative satisfies e prime(t)<=-2 alpha e(t). Differentiability makes f continuous, so the supplied continuity of X makes e continuous on the closed interval. Each right derivative supplies the one-sided slope hypothesis for Mathlib Gronwall on [0,T]. With constant coefficient -2 alpha and zero forcing, its bound is e(0) exp(-2 alpha t), including the terminal endpoint. The global minimum gives e(t)>=0.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem dissipation_and_decay {f : E → ℝ} {X : ℝ → E} {z : E} {α T : ℝ}
    (_hα : 0 < α) (_hT : 0 ≤ T) (hf : Differentiable ℝ f)
    (hX : ContinuousOn X (Icc 0 T))
    (hflow : ∀ t ∈ Ico 0 T,
      HasDerivWithinAt X (-gradient f (X t)) (Ici t) t)
    (hz : IsMinOn f univ z)
    (hpl : ∀ x, 2 * α * (f x - f z) ≤ ‖gradient f x‖ ^ 2) :
    (∀ t ∈ Ico 0 T, HasDerivWithinAt (f ∘ X)
      (-‖gradient f (X t)‖ ^ 2) (Ici t) t) ∧
    ∀ t ∈ Icc 0 T, 0 ≤ f (X t) - f z ∧
      f (X t) - f z ≤ (f (X 0) - f z) * Real.exp (-2 * α * t) := by
  have hd : ∀ t ∈ Ico 0 T, HasDerivWithinAt (f ∘ X)
      (-‖gradient f (X t)‖ ^ 2) (Ici t) t := by
    intro t ht
    have hgrad : HasFDerivAt f (InnerProductSpace.toDual ℝ E (gradient f (X t))) (X t) :=
      (hf (X t)).hasGradientAt
    have h := hgrad.comp_hasDerivWithinAt t (hflow t ht)
    simpa only [InnerProductSpace.toDual_apply_apply, inner_neg_right,
      real_inner_self_eq_norm_sq] using h
  refine ⟨hd, ?_⟩
  intro t ht
  refine ⟨sub_nonneg.mpr (hz (mem_univ (X t))), ?_⟩
  have hc : ContinuousOn (fun u => f (X u) - f z) (Icc 0 T) :=
    (hf.continuous.comp_continuousOn hX).sub continuousOn_const
  have hg := le_gronwallBound_of_liminf_deriv_right_le
    (f := fun u => f (X u) - f z) (f' := fun u => -‖gradient f (X u)‖ ^ 2)
    (δ := f (X 0) - f z) (K := -(2 * α)) (ε := 0) hc
    (fun u hu r hr => by
      simpa [Function.comp_def, slope] using
        ((hd u hu).sub_const (f z)).liminf_right_slope_le hr)
    le_rfl
    (fun u _ => by nlinarith [hpl (X u)]) t ht
  simpa [gronwallBound_ε0, sub_zero, neg_mul] using hg

end AutoSamplingTheory.TechnicalLemmas.Analysis.GradientFlowPL

Exact module and namespace context

Put D(t)=Y(t)-X(t). Subtract the two actual right ODE derivatives, then differentiate the smooth squared norm. This remains valid when the two points coincide, so no division by their distance is needed. Differentiability identifies the actual gradient. The existing shared result derives gradient monotonicity from the global strong-convex chord inequality. Applied at X(t) and Y(t), it bounds the squared-separation derivative by -2 alpha times the squared separation. Continuity of both curves gives continuity of the squared separation including endpoints. Right derivatives provide the one-sided slope hypothesis of the existing interval Gronwall bound. Zero forcing yields the squared-distance estimate. Both the norm and exponential multiple of the initial norm are nonnegative; comparing their squares gives the exact alpha rate.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem norm_sub_le {f : E → ℝ} {X Y : ℝ → E} {α T : ℝ}
    (_hα : 0 ≤ α) (_hT : 0 ≤ T) (hf : Differentiable ℝ f)
    (hsc : StrongConvexOn univ α f)
    (hX : ContinuousOn X (Icc 0 T)) (hY : ContinuousOn Y (Icc 0 T))
    (hx : ∀ t ∈ Ico 0 T, HasDerivWithinAt X (-gradient f (X t)) (Ici t) t)
    (hy : ∀ t ∈ Ico 0 T, HasDerivWithinAt Y (-gradient f (Y t)) (Ici t) t) :
    ∀ t ∈ Icc 0 T, ‖Y t - X t‖ ≤ Real.exp (-α * t) * ‖Y 0 - X 0‖ := by
  have hd (t : ℝ) (ht : t ∈ Ico 0 T) :
      HasDerivWithinAt (fun u => ‖Y u - X u‖ ^ 2)
        (-2 * inner ℝ (gradient f (Y t) - gradient f (X t)) (Y t - X t))
        (Ici t) t := by
    have h := ((hy t ht).sub (hx t ht)).norm_sq
    simp only [Pi.sub_apply] at h
    rw [show -gradient f (Y t) - -gradient f (X t) =
      -(gradient f (Y t) - gradient f (X t)) by abel,
      inner_neg_right, real_inner_comm] at h
    convert h using 1; ring
  intro t ht
  have hg := le_gronwallBound_of_liminf_deriv_right_le
    (f := fun u => ‖Y u - X u‖ ^ 2)
    (f' := fun u => -2 * inner ℝ (gradient f (Y u) - gradient f (X u)) (Y u - X u))
    (δ := ‖Y 0 - X 0‖ ^ 2) (K := -(2 * α)) (ε := 0)
    ((hY.sub hX).norm.pow 2)
    (fun u hu r hr => by simpa [slope] using (hd u hu).liminf_right_slope_le hr)
    le_rfl (fun u _ => by
      have hm := StrongConvexFirstOrder.gradient_inner_lower_bound_of_strongConvexOn
        hsc (fun z _ => (hf z).hasGradientAt) (mem_univ (X u)) (mem_univ (Y u))
      nlinarith) t ht
  have hs : ‖Y t - X t‖ ^ 2 ≤ (Real.exp (-α * t) * ‖Y 0 - X 0‖) ^ 2 := by
    rw [mul_pow, show Real.exp (-α * t) ^ 2 = Real.exp (-(2 * α) * t) by
      rw [sq, ← Real.exp_add]; congr 1; ring, mul_comm]
    simpa only [gronwallBound_ε0, sub_zero] using hg
  exact (sq_le_sq₀ (norm_nonneg _) (mul_nonneg (Real.exp_pos _).le (norm_nonneg _))).mp hs

end AutoSamplingTheory.TechnicalLemmas.Analysis.GradientFlowContraction

Exact module and namespace context

Represent the derivative of f by its gradient, compose with the actual right derivative of X, and obtain minus the squared gradient norm. On each subinterval [a,b], scalar Gronwall with zero coefficient and zero forcing proves f(X(b))<=f(X(a)). This uses continuity at both endpoints and only right derivatives before b. Fix an observation time t and put r(s)=norm(X(s)-z) squared, e(s)=f(X(s))-f(z). Differentiate r using the actual ODE. The existing first-order strong-convexity inequality at X(s) with comparator z gives r prime<=-alpha r-2e(s). Descent implies e(s)>=e(t) for s<=t, so the forcing can be bounded by the fixed constant -2e(t). Apply existing scalar interval Gronwall to r on [0,t] with coefficient -alpha and forcing -2e(t). The scalar version permits negative forcing. Nonnegativity of r(t) gives the left side of each displayed bound. Alpha=0 is evaluated directly; no zero denominator is substituted into the other branch. For t>0, the zero branch divides by 2t. In the positive branch multiply by alpha exp(alpha t), use exp(-alpha t)exp(alpha t)=1, then divide by 2(exp(alpha t)-1)>0. The supplied global minimum gives a nonnegative objective gap.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem value_le {f : E → ℝ} {X : ℝ → E} {z : E} {α T : ℝ}
    (hα : 0 ≤ α) (_hT : 0 ≤ T) (hf : Differentiable ℝ f)
    (hsc : StrongConvexOn 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) :
    ∀ t ∈ Ioc 0 T, 0 ≤ f (X t) - f z ∧
      f (X t) - f z ≤ if α = 0 then ‖X 0 - z‖ ^ 2 / (2 * t)
        else α / (2 * (Real.exp (α * t) - 1)) * ‖X 0 - z‖ ^ 2 := by
  have hd (u : ℝ) (hu : u ∈ Ico 0 T) :
      HasDerivWithinAt (fun s => f (X s)) (-‖gradient f (X u)‖ ^ 2) (Ici u) u := by
    have hgrad : HasFDerivAt f (InnerProductSpace.toDual ℝ E (gradient f (X u))) (X u) :=
      (hf (X u)).hasGradientAt
    simpa only [Function.comp_def, InnerProductSpace.toDual_apply_apply,
      inner_neg_right, real_inner_self_eq_norm_sq] using
      hgrad.comp_hasDerivWithinAt u (hflow u hu)
  have hmono : AntitoneOn (fun s => f (X s)) (Icc 0 T) := by
    intro a ha b hb hab
    have hc := (hf.continuous.comp_continuousOn hX).mono
      (show Icc a b ⊆ Icc 0 T from fun u hu => ⟨ha.1.trans hu.1, hu.2.trans hb.2⟩)
    have hg := le_gronwallBound_of_liminf_deriv_right_le
      (f' := fun u => -‖gradient f (X u)‖ ^ 2) (δ := f (X a)) (K := 0) (ε := 0) hc
      (fun u hu r hr => by
        simpa [slope] using (hd u ⟨ha.1.trans hu.1, hu.2.trans_le hb.2⟩).liminf_right_slope_le hr)
      le_rfl (fun u _ => by nlinarith [sq_nonneg ‖gradient f (X u)‖]) b ⟨hab, le_rfl⟩
    simpa [gronwallBound_K0] using hg
  have hdist (u : ℝ) (hu : u ∈ Ico 0 T) :
      HasDerivWithinAt (fun s => ‖X s - z‖ ^ 2)
        (-2 * inner ℝ (gradient f (X u)) (X u - z)) (Ici u) u := by
    have h := ((hflow u hu).sub_const z).norm_sq
    simp only [inner_neg_right, real_inner_comm] at h
    convert h using 1; ring
  intro t ht
  refine ⟨sub_nonneg.mpr (hz (mem_univ _)), ?_⟩
  have hbound := le_gronwallBound_of_liminf_deriv_right_le
    (f := fun s => ‖X s - z‖ ^ 2)
    (f' := fun u => -2 * inner ℝ (gradient f (X u)) (X u - z))
    (δ := ‖X 0 - z‖ ^ 2) (K := -α) (ε := -2 * (f (X t) - f z))
    (((hX.sub continuousOn_const).norm.pow 2).mono
      (show Icc 0 t ⊆ Icc 0 T from fun u hu => ⟨hu.1, hu.2.trans ht.2⟩))
    (fun u hu r hr => by
      simpa [slope] using (hdist u ⟨hu.1, hu.2.trans_le ht.2⟩).liminf_right_slope_le hr)
    le_rfl (fun u hu => by
      have hs := StrongConvexFirstOrder.firstOrder_lower_bound_of_strongConvexOn
        hsc (fun x _ => (hf x).hasGradientAt) (mem_univ (X u)) (mem_univ z)
      rw [show z - X u = -(X u - z) by abel, inner_neg_right, norm_neg] at hs
      have hm := hmono ⟨hu.1, hu.2.le.trans ht.2⟩ ⟨ht.1.le, ht.2⟩ hu.2.le
      nlinarith) t ⟨ht.1.le, le_rfl⟩
  have hn := (sq_nonneg ‖X t - z‖).trans hbound
  by_cases ha : α = 0
  · simp only [ha, neg_zero, gronwallBound_K0, sub_zero] at hn ⊢
    apply (le_div_iff₀ (mul_pos (by norm_num) ht.1)).mpr
    nlinarith
  · rw [if_neg ha]
    have hap : 0 < α := lt_of_le_of_ne hα (Ne.symm ha)
    rw [gronwallBound_of_K_ne_0 (neg_ne_zero.mpr ha), sub_zero] at hn
    have hmul := mul_nonneg hn hap.le
    have heq : (‖X 0 - z‖ ^ 2 * Real.exp (-α * t) +
        (-2 * (f (X t) - f z)) / -α * (Real.exp (-α * t) - 1)) * α =
        α * ‖X 0 - z‖ ^ 2 * Real.exp (-α * t) +
          2 * (f (X t) - f z) * (Real.exp (-α * t) - 1) := by
      field_simp
    rw [heq] at hmul
    have he : Real.exp (-α * t) * Real.exp (α * t) = 1 := by
      rw [← Real.exp_add, show -α * t + α * t = 0 by ring, Real.exp_zero]
    have hp := mul_nonneg hmul (Real.exp_pos (α * t)).le
    have hcancel : (α * ‖X 0 - z‖ ^ 2 * Real.exp (-α * t) +
        2 * (f (X t) - f z) * (Real.exp (-α * t) - 1)) * Real.exp (α * t) =
        α * ‖X 0 - z‖ ^ 2 - 2 * (f (X t) - f z) * (Real.exp (α * t) - 1) := by
      calc
        _ = α * ‖X 0 - z‖ ^ 2 * (Real.exp (-α * t) * Real.exp (α * t)) +
          2 * (f (X t) - f z) * (Real.exp (-α * t) * Real.exp (α * t)) -
          2 * (f (X t) - f z) * Real.exp (α * t) := by ring
        _ = _ := by rw [he]; ring
    rw [hcancel] at hp
    rw [div_mul_eq_mul_div]
    apply (le_div_iff₀ (mul_pos (by norm_num) (sub_pos.mpr (Real.one_lt_exp_iff.mpr
      (mul_pos hap ht.1))))).mpr
    nlinarith

end AutoSamplingTheory.TechnicalLemmas.Analysis.GradientFlowValue

Exact module and namespace context

The C1 assumption makes the Frechet derivative continuous. The Riesz inverse is continuous, so the actual gradient, and hence its norm along X, is continuous. The nonempty compact time interval therefore contains a minimizing time s. Put m=norm(gradient f(X(s))). Compose the Frechet derivative of f with the supplied right derivative of X. The gradient ODE makes the resulting inner product minus the squared gradient norm. Minimality of m bounds that derivative above by -m squared. Integrating this constant derivative bound gives f(X(T))<=f(X(0))-T m squared. In Lean the existing scalar right-slope Gronwall theorem with coefficient zero and forcing -m squared performs this comparison. The supplied minimum gives f(z)<=f(X(T)), so T m squared cannot exceed the initial objective gap. Divide by the strictly positive T, then take the nonnegative square root. Because s was chosen as a minimizer, this bounds the attained minimum over the whole time interval, not necessarily the gradient at its final time.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem exists_min_norm_le {f : E → ℝ} {X : ℝ → E} {z : E} {T : ℝ}
    (hT : 0 < T) (hf : ContDiff ℝ 1 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) :
    ∃ s ∈ Icc 0 T, IsMinOn (fun u => ‖gradient f (X u)‖) (Icc 0 T) s ∧
      ‖gradient f (X s)‖ ≤ Real.sqrt ((f (X 0) - f z) / T) := by
  have hdf : Differentiable ℝ f := hf.differentiable (by norm_num)
  have hcg : Continuous (gradient f) :=
    (InnerProductSpace.toDual ℝ E).symm.continuous.comp (hf.continuous_fderiv (by norm_num))
  obtain ⟨s, hs, hmin⟩ := isCompact_Icc.exists_isMinOn
    (nonempty_Icc.mpr hT.le) (hcg.comp_continuousOn hX).norm
  refine ⟨s, hs, hmin, ?_⟩
  have hd (u : ℝ) (hu : u ∈ Ico 0 T) :
      HasDerivWithinAt (fun v => f (X v)) (-‖gradient f (X u)‖ ^ 2) (Ici u) u := by
    have hg : HasFDerivAt f (InnerProductSpace.toDual ℝ E (gradient f (X u))) (X u) :=
      (hdf (X u)).hasGradientAt
    simpa only [Function.comp_def, InnerProductSpace.toDual_apply_apply,
      inner_neg_right, real_inner_self_eq_norm_sq] using
      hg.comp_hasDerivWithinAt u (hflow u hu)
  have hb := le_gronwallBound_of_liminf_deriv_right_le
    (f' := fun u => -‖gradient f (X u)‖ ^ 2) (δ := f (X 0))
    (K := 0) (ε := -‖gradient f (X s)‖ ^ 2)
    (hf.continuous.comp_continuousOn hX)
    (fun u hu r hr => by simpa [slope] using (hd u hu).liminf_right_slope_le hr)
    le_rfl (fun u hu => by
      have hm := hmin (show u ∈ Icc 0 T from ⟨hu.1, hu.2.le⟩)
      have hsq := sq_le_sq₀ (norm_nonneg (gradient f (X s))) (norm_nonneg (gradient f (X u)))
      simpa using (neg_le_neg (hsq.mpr hm))) T ⟨hT.le, le_rfl⟩
  simp only [gronwallBound_K0, sub_zero] at hb
  apply (Real.le_sqrt (norm_nonneg _) (div_nonneg
    (sub_nonneg.mpr (hz (mem_univ _))) hT.le)).mpr
  apply (le_div_iff₀ hT).mpr
  have hzT : f z ≤ f (X T) := hz (mem_univ (X T))
  change f (X T) ≤ _ at hb
  nlinarith

end AutoSamplingTheory.TechnicalLemmas.Analysis.GradientFlowStationarity

Exact module and namespace context

The existing first-order convexity theorem gives gradient monotonicity. The compiled gradient-Hessian equivalence turns it into nonnegativity of the true second Frechet derivative on every diagonal direction. Compose the derivative of Df with the inverse Riesz map to obtain the actual derivative H(x) of gradient f. Then inner(H(x)v,v)>=0. No Hessian sign or independent gradient field is supplied. Write g(t)=gradient f(X(t)), e(t)=f(X(t))-f(z), r(t)=norm(X(t)-z) squared. The actual right gradient ODE gives the three identities below. They are derived by chain and product rules, including differentiation of the actual gradient via H. Differentiate L(t)=t squared norm(g) squared+2t e+r. The two opposite 2t norm(g) squared terms cancel. The Hessian term is nonpositive; first-order support gives e<=inner(g,X-z). Therefore the actual right derivative of L is nonpositive. Scalar K0, zero-forcing Gronwall on every subinterval [a,b] proves L(b)<=L(a). For positive t, global minimality makes e(t) nonnegative, and r(t) is a squared norm. Drop these two nonnegative terms from L(t)<=L(0). Divide by t squared, which is strictly positive. First-order support and Cauchy-Schwarz bound e by norm(g) norm(X-z). Young inequality, obtained by squaring t norm(g)-norm(X-z), then gives 2t e<=t squared norm(g) squared+r. Hence 4t e<=L(t)<=L(0). Division by 4t yields the exact improved upper coefficient.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

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,
        real_inner_self_eq_norm_sq] using h.comp_hasDerivWithinAt t (hflow t ht)
    have hr := ((hflow t ht).sub_const z).norm_sq
    have hid := (hasDerivAt_id t).hasDerivWithinAt (s := Ici t)
    convert (((hid.pow 2).mul hn).add ((hid.const_mul 2).mul (he.sub_const (f z)))).add hr using 1 <;>
      first | rfl | (simp only [D, Function.comp_def, id_eq, Pi.pow_apply, Nat.cast_ofNat,
        show (2 : ℕ) - 1 = 1 by decide, pow_one, mul_one, ContinuousLinearMap.map_neg,
        inner_neg_right, real_inner_comm]; ring)
  have hneg (t : ℝ) : D t ≤ 0 := by
    have hh := mul_nonneg (sq_nonneg t) (hpos (X t) (gradient f (X t)))
    have hs := hsupp (X t)
    dsimp [D]
    nlinarith
  have hm : AntitoneOn L (Icc 0 T) := by
    intro a ha b hb hab
    have h := le_gronwallBound_of_liminf_deriv_right_le (f' := D)
      (δ := L a) (K := 0) (ε := 0)
      (hcont.mono (show Icc a b ⊆ Icc 0 T from fun u hu => ⟨ha.1.trans hu.1, hu.2.trans hb.2⟩))
      (fun u hu r hr => by simpa [slope] using
        (hd u ⟨ha.1.trans hu.1, hu.2.trans_le hb.2⟩).liminf_right_slope_le hr)
      le_rfl (fun u _ => by simpa using hneg u) b ⟨hab, le_rfl⟩
    simpa [gronwallBound_K0] using h
  refine ⟨hm, ?_⟩
  intro t ht
  have hL := hm ⟨le_rfl, hT⟩ ⟨ht.1.le, ht.2⟩ ht.1.le
  simp only [L, zero_pow (by decide : 2 ≠ 0), zero_mul, zero_add] at hL
  have he : 0 ≤ f (X t) - f z := sub_nonneg.mpr (hz (mem_univ _))
  have hte := mul_nonneg ht.1.le he
  refine ⟨(le_div_iff₀ (sq_pos_of_pos ht.1)).mpr (by nlinarith [sq_nonneg ‖X t - z‖]), ?_⟩
  have hs := hsupp (X t)
  have hcs := real_inner_le_norm (gradient f (X t)) (X t - z)
  have hts := mul_le_mul_of_nonneg_left (hs.trans hcs) ht.1.le
  have hy := sq_nonneg (t * ‖gradient f (X t)‖ - ‖X t - z‖)
  apply (le_div_iff₀ (mul_pos (by norm_num) ht.1)).mpr
  nlinarith

end AutoSamplingTheory.TechnicalLemmas.Analysis.GradientFlowLastIterate

Exact module and namespace context