theorem ERealFunction.subdifferential_infimalConvolution_eq_singleton_of_mem_dom_of_value_eq_of_gateauxDerivative {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (f g : H → ↑(Set.Ioi ⊥)) (hf : f ∈ Γ₀(H)) (hg : g ∈ Γ₀(H)) (x y gradf : H) (hx : x ∈ (subdifferential ((fun (f g : H → ↑(Set.Ioi ⊥)) (x : H) => infimalConvolution (fun (y : H) => ↑(f y)) (fun (y : H) => ↑(g y)) x) f g)).dom) (hEq : (fun (f g : H → ↑(Set.Ioi ⊥)) (x : H) => infimalConvolution (fun (y : H) => ↑(f y)) (fun (y : H) => ↑(g y)) x) f g x = ↑(f y) + ↑(g (x - y))) (hgrad : HasGateauxDerivativeAt (fun (z : H) => (↑(f z)).toReal) ((InnerProductSpace.toDual ℝ H) gradf) y) : subdifferential ((fun (f g : H → ↑(Set.Ioi ⊥)) (x : H) => infimalConvolution (fun (y : H) => ↑(f y)) (fun (y : H) => ↑(g y)) x) f g) x = {gradf}

Proposition 18.6: if x belongs to the domain of the subdifferential of the infimal convolution f □ g, the infimal convolution is exact at x with minimizer y, and f has Gâteaux gradient gradf at y, then the subdifferential of f □ g at x is the singleton {gradf}.