PL gradient flows decrease the objective exponentially
AutoSamplingTheory.TechnicalLemmas.Analysis.GradientFlowPL.dissipation_and_decay · theorem · Teaching coverage
Statement
Let E be a complete real inner-product space, f:E→R be Frechet differentiable everywhere, z a global minimizer, alpha>0 and T>=0. Let X:R→E be continuous on [0,T] and have right derivative -gradient f(X(t)) for every t in [0,T). Assume the global numerical PL inequality below. Then the actual objective has the stated right derivative before T, and its nonnegative gap satisfies the exponential bound at every t in [0,T].
All objects and hypotheses
- E is a complete real inner-product space; f is Frechet differentiable at every point.
- Alpha>0 and T>=0; f(z)<=f(x) for every x:E.
- X is continuous on [0,T]; for each t in [0,T), HasDerivWithinAt X (-gradient f(X(t))) (Ici t) t. No negative-time derivative is required.
- For every x:E, 2 alpha (f(x)-f(z))<=norm gradient f(x) squared.
Mathematical proof
1. Differentiate the actual objective along the curve
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.
Corresponding Lean step
DifferentiableAt.hasGradientAt, HasFDerivAt.comp_hasDerivWithinAt, InnerProductSpace.toDual_apply_apply, inner_neg_right, real_inner_self_eq_norm_sq.
2. Convert PL into a differential inequality
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).
Corresponding Lean step
HasDerivWithinAt.sub_const and the supplied PL inequality, with rate exactly 2*alpha.
3. Apply the existing interval comparison and retain endpoints
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.
Corresponding Lean step
Continuous.comp_continuousOn, HasDerivWithinAt.liminf_right_slope_le, le_gronwallBound_of_liminf_deriv_right_le, gronwallBound_ε0, IsMinOn.
Lean statement · dissipation_and_decay
Actual objective right derivative and nonnegative PL gap decay on a finite forward interval.
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)Lean proof · dissipation_and_decay
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.GradientFlowPLScope and omitted-condition boundaries
- The objective is generalized from the source finite Euclidean C2 setting to an everywhere Frechet differentiable function on a complete real Hilbert space. The proof requires the actual derivative, not a supplied scalar dissipation identity. It does not assert continuous differentiability of the gradient.
- A supplied continuous curve is considered on [0,T], T>=0. Its right gradient-flow derivative is assumed only for 0<=t<T. Terminal continuity is retained, but no derivative at T, negative-time dynamics, existence, uniqueness or extension of the flow is asserted. For T=0 the rate is equality and the derivative conclusion is vacuous.
- The source positive PL modulus and attained minimum are explicit. The minimum supplies nonnegative gap; positivity specifies the exponential-decay regime although the comparison algebra also works without that sign. No convexity, point-distance rate, gradient Lipschitzness, discretization, stochastic flow or companion-paper theorem is concluded.
Source and reuse
ASTIS parents called
Mathlib API called (external library)
- HasFDerivAt.comp_hasDerivWithinAt
- DifferentiableAt.hasGradientAt
- HasDerivWithinAt.liminf_right_slope_le
- le_gronwallBound_of_liminf_deriv_right_le
- gronwallBound_ε0
Mathematical sources
- Chewi Lemma2.1 and Corollary2.6 — Supplied gradient dynamics and positive PL modulus; no well-posedness theorem.
- Nonstationary quadratic flow — Actual X(t)=exp(-t), f(x)=x squared/2, with proved gradient, PL, minimum and sharp rate.
ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.