theorem ERealFunction.infimalConvolution_eq_infimalPostcomposition_separableSum {H : Type u} [AddCommGroup H] (f g : H → ↑(Set.Ioi ⊥)) : infimalConvolution (Function.asEReal f) (Function.asEReal g) = (fun (L : H × H → H) (f : H × H → ↑(Set.Ioi ⊥)) (y : H) => infimalPostcomposition L (fun (x : H × H) => ↑(f x)) y) (Prod.fst + Prod.snd) ((fun (f g : H → ↑(Set.Ioi ⊥)) => pointwiseAdd (f ∘ Prod.fst) (g ∘ Prod.snd)) f g)

Proposition 12.37: infimal convolution is the infimal postcomposition of the separable sum (y, z) ↦ f y + g z by the product-sum map (y, z) ↦ y + z.