theorem ERealFunction.fitzpatrickFunction_subdifferential_le_separableSum_gammaZeroConjugate {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (f : H → ↑(Set.Ioi ⊥)) (hf : f ∈ Γ₀(H)) : (subdifferential f).fitzpatrickFunction ≤ Function.asEReal ((fun (f g : H → ↑(Set.Ioi ⊥)) => pointwiseAdd (f ∘ Prod.fst) (g ∘ Prod.snd)) f (gammaZeroConjugate f hf))

The Fitzpatrick function of the subdifferential of a Γ₀(H) function is bounded above by the separable sum f ⊕ f*, represented in the project by the canonical packaged conjugate f∗[hf].

theorem ERealFunction.dom_prod_gammaZeroConjugate_subset_dom_fitzpatrickFunction_subdifferential {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (f : H → ↑(Set.Ioi ⊥)) (hf : f ∈ Γ₀(H)) : effectiveDomain f ×ˢ effectiveDomain (gammaZeroConjugate f hf) ⊆ dom (subdifferential f).fitzpatrickFunction

Any pair of finite points for f and its Fenchel conjugate f*, represented by the canonical packaged conjugate f∗[hf], lies in the domain of the Fitzpatrick function of ∂ f.

theorem ERealFunction.fitzpatrickFunction_subdifferential_le_separableSum_gammaZeroConjugate_and_dom_prod_subset {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (f : H → ↑(Set.Ioi ⊥)) (hf : f ∈ Γ₀(H)) : (subdifferential f).fitzpatrickFunction ≤ Function.asEReal ((fun (f g : H → ↑(Set.Ioi ⊥)) => pointwiseAdd (f ∘ Prod.fst) (g ∘ Prod.snd)) f (gammaZeroConjugate f hf)) ∧ effectiveDomain f ×ˢ effectiveDomain (gammaZeroConjugate f hf) ⊆ dom (subdifferential f).fitzpatrickFunction

Example 20.55: if f ∈ Γ₀(H), then F_{∂ f} ≤ f ⊕ f* and dom f × dom f* ⊆ dom F_{∂ f}, where f* is represented by the canonical packaged conjugate f∗[hf].