theorem ERealFunction.moreauQuadraticKernel_eq_moreauEnvelope_add_conjugateMoreauEnvelope {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (f : H → ↑(Set.Ioi ⊥)) (hf : f ∈ Γ₀(H)) (γ : PosReal) : Function.asEReal (moreauQuadraticKernel γ) = {}^[γ]f + {}^[γ⁻¹](conjugate (Function.asEReal f)) ∘ fun (x : H) => (↑γ)⁻¹ • x

Theorem 14.3 (1): for f ∈ Γ₀(H) and γ ∈ ℝ_{++}, equation (14.3) states that the quadratic kernel γ⁻¹ q is the sum of the γ-Moreau envelope of f and the γ⁻¹-Moreau envelope of f* composed with γ⁻¹ Id.

theorem ERealFunction.id_eq_scaledProximityOperator_add_scaledProximityOperator_conjugate {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (f : H → ↑(Set.Ioi ⊥)) (hf : f ∈ Γ₀(H)) (γ : PosReal) : id = Prox[γ, f, hf] + ↑γ • Prox[γ⁻¹, gammaZeroConjugate f hf, ⋯] ∘ fun (x : H) => (↑γ)⁻¹ • x

Theorem 14.3 (2): Moreau's decomposition gives the operator identity Id = Prox_{γ f} + γ Prox_{f^* / γ} ∘ γ⁻¹ Id.

theorem ERealFunction.proxValue_add_conjugateProxValue_eq_inner {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (f : H → ↑(Set.Ioi ⊥)) (hf : f ∈ Γ₀(H)) (γ : PosReal) (x p pStar : H) (hp : p = Prox[γ, f, hf] x) (hpStar : pStar = Prox[γ⁻¹, gammaZeroConjugate f hf, ⋯] ((↑γ)⁻¹ • x)) : ↑(f p) + conjugate (Function.asEReal f) pStar = ↑(inner ℝ p pStar)

Theorem 14.3 (3): if p = Prox_{γ f} x and p* = Prox_{f^* / γ} (x / γ), then equation (14.4) gives f p + f^*(p*) = ⟪p, p*⟫.