def ERealFunction.HasLipschitzGradient {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (f : H → ℝ) (β : ↑(Set.Ioi 0)) : Prop

Differentiability together with β-Lipschitz continuity of the gradient.

def ERealFunction.HasGradientInnerQuadraticUpperBound {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (f : H → ℝ) (β : ↑(Set.Ioi 0)) : Prop

Differentiability together with the quadratic upper bound on the gradient increment.

def ERealFunction.HasQuadraticDescentEstimate {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (f : H → ℝ) (β : ↑(Set.Ioi 0)) : Prop

Differentiability together with the quadratic descent estimate.

def ERealFunction.HasConjugateGradientQuadraticLowerBound {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (f : H → ℝ) (β : ↑(Set.Ioi 0)) : Prop

Differentiability together with the Fenchel-conjugate quadratic lower bound along the gradient image.

def ERealFunction.HasCocoerciveGradient {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (f : H → ℝ) (β : ↑(Set.Ioi 0)) : Prop

Differentiability together with 1 / β-cocoercivity of the gradient on the whole space.

def ERealFunction.HasHalfSquaredNormSubConvexity {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (f : H → ℝ) (β : ↑(Set.Ioi 0)) : Prop

Convexity of the shifted quadratic β q - f, with q(x) = ‖x‖² / 2.

def ERealFunction.HasShiftedConjugateConvexity {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (f : H → ℝ) (β : ↑(Set.Ioi 0)) : Prop

Convexity of the shifted conjugate f* - β⁻¹ q on its effective domain.

structure ERealFunction.HasMoreauEnvelopeRepresentation {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (f : H → ℝ) (β : ↑(Set.Ioi 0)) : Prop

The Moreau-envelope representation attached to the shifted conjugate f* - β⁻¹ q.

• mem_gammaZero : conjugateSubInvHalfSquaredNorm f β ∈ Γ₀(H)
• primal_moreau_eq : Function.asEReal (Function.toEReal f) = {}^[β⁻¹](gammaZeroConjugate (conjugateSubInvHalfSquaredNorm f β) ⋯)
• dual_moreau_eq : Function.asEReal (Function.toEReal f) = Function.asEReal (moreauQuadraticKernel β⁻¹) - {}^[β](conjugateSubInvHalfSquaredNorm f β) ∘ fun (x : H) => ↑β • x

structure ERealFunction.HasProximalGradientRepresentation {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (f : H → ℝ) (β : ↑(Set.Ioi 0)) : Prop

The proximal-operator formulas for the gradient attached to the shifted conjugate f* - β⁻¹ q.

• mem_gammaZero : conjugateSubInvHalfSquaredNorm f β ∈ Γ₀(H)
• gradient_eq_scaledProximityOperator : gradient f = fun (x : H) => Prox[β, conjugateSubInvHalfSquaredNorm f β, ⋯] (↑β • x)
• gradient_eq_smul_sub_scaledProximityOperator_gammaZeroConjugate : gradient f = fun (x : H) => ↑β • (x - Prox[β⁻¹, gammaZeroConjugate (conjugateSubInvHalfSquaredNorm f β) ⋯, ⋯] x)

theorem ERealFunction.frechetDifferentiable_tfae_lipschitz_gradient {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (f : H → ℝ) (hcont : Continuous f) (hconv : _root_.ConvexOn ℝ Set.univ f) (β : ↑(Set.Ioi 0)) : [HasLipschitzGradient f β, HasGradientInnerQuadraticUpperBound f β, HasQuadraticDescentEstimate f β, HasConjugateGradientQuadraticLowerBound f β, HasCocoerciveGradient f β, HasHalfSquaredNormSubConvexity f β, HasShiftedConjugateConvexity f β, HasMoreauEnvelopeRepresentation f β, HasProximalGradientRepresentation f β].TFAE

Theorem 18.15: for a continuous convex function f : H → ℝ, a positive parameter β, and h = f* - β⁻¹ q with q(x) = ‖x‖² / 2, the standard smoothness, descent, cocoercivity, convexity, and proximal formulations of β-Lipschitz differentiability are equivalent.