Two gradient flows contract under strong convexity
AutoSamplingTheory.TechnicalLemmas.Analysis.GradientFlowContraction.norm_sub_le · theorem · Teaching coverage
Statement
Let E be a complete real inner-product space and f:E→R be Frechet differentiable everywhere. Let alpha>=0 and T>=0, and assume f is globally alpha-convex in the chord sense. Let X,Y:R→E be continuous on [0,T], with right derivatives -gradient f(X(t)) and -gradient f(Y(t)) for every 0<=t<T. Then the distance between the trajectories satisfies the following bound for every 0<=t<=T.
All objects and hypotheses
- Complete real inner-product space E; f is Frechet differentiable everywhere.
- Alpha>=0, T>=0, and StrongConvexOn univ alpha f with the alpha/2 chord normalization.
- X and Y are continuous on the closed interval [0,T]; their actual right ODE derivatives exist at every point of [0,T).
Mathematical proof
1. Differentiate squared separation
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.
Corresponding Lean step
HasDerivWithinAt.sub and HasDerivWithinAt.norm_sq; inner_neg_right and real_inner_comm.
2. Reuse the strong-convex gradient bound
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.
Corresponding Lean step
StrongConvexFirstOrder.gradient_inner_lower_bound_of_strongConvexOn, with DifferentiableAt.hasGradientAt.
3. Compare on the closed interval and take square roots
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.
Corresponding Lean step
HasDerivWithinAt.liminf_right_slope_le, le_gronwallBound_of_liminf_deriv_right_le, gronwallBound_ε0, Real.exp_add and sq_le_sq₀.
Lean statement · norm_sub_le
Finite-interval pairwise norm contraction for actual gradient flows.
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‖Lean proof · norm_sub_le
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.GradientFlowContractionScope and omitted-condition boundaries
- The source C2 Euclidean objective is generalized to an everywhere Frechet differentiable objective on a complete real Hilbert space. StrongConvexOn univ alpha f is the global chord inequality with alpha/2 normalization. Alpha>=0 retains Definition1.5: positive alpha contracts exponentially and zero alpha is nonexpansive.
- The two curves are supplied and continuous on [0,T], T>=0, with actual right derivatives equal to the negative gradient on [0,T). Ordinary source flows restrict to these hypotheses. Terminal continuity is retained; no derivative at T or negative-time dynamics is assumed. T=0 gives equality.
- The source standing attained-minimum convention is unnecessary for this pairwise estimate and is omitted explicitly. There is no flow existence, extension, minimizer construction, discrete algorithm, stochastic coupling, Wasserstein or companion-paper result. No nonzero separation or gradient Lipschitz premise is used.
Source and reuse
ASTIS parents called
Mathlib API called (external library)
- HasDerivWithinAt.norm_sq
- DifferentiableAt.hasGradientAt
- HasDerivWithinAt.liminf_right_slope_le
- le_gronwallBound_of_liminf_deriv_right_le
- gronwallBound_ε0
- sq_le_sq₀
Mathematical sources
- Chewi Theorem2.2 — Pairwise contraction from actual gradient dynamics; Definition1.5 nonnegative curvature convention.
- Sharp quadratic trajectories and zero curvature — Proves the actual ODE and strong convexity for f(x)=x squared/2, with arbitrary initial positions, plus a zero-curvature constant-objective case.
ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.