theorem ERealFunction.dom_infimalConvolution {H : Type u} [AddGroup H] (f g : H → ↑(Set.Ioi ⊥)) : dom ((fun (f g : H → ↑(Set.Ioi ⊥)) (x : H) => infimalConvolution (fun (y : H) => ↑(f y)) (fun (y : H) => ↑(g y)) x) f g) = effectiveDomain f + effectiveDomain g

Proposition 12.6 (ii): for extended-real-valued functions that never take the value -∞, the domain of the infimal convolution is the Minkowski sum of the domains.

theorem ERealFunction.infimalConvolution_comm {H : Type u} [AddCommGroup H] (f g : H → EReal) : infimalConvolution f g = infimalConvolution g f

Proposition 12.6 (iii): infimal convolution is commutative.

theorem ERealFunction.hasContinuousAffineMinorantWithSlope_infimalConvolution {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (f g : H → EReal) (u : H) (hf : HasContinuousAffineMinorantWithSlope f u) (hg : HasContinuousAffineMinorantWithSlope g u) : HasContinuousAffineMinorantWithSlope ((fun (f g : H → EReal) (x : H) => infimalConvolution (fun (y : H) => f y) (fun (y : H) => g y) x) f g) u

Proposition 12.6 (i): if f and g admit continuous affine minorants with slope u, then their infimal convolution admits one with the same slope.

theorem ERealFunction.infimalConvolution_ne_bot_of_hasContinuousAffineMinorantWithSlope {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (f g : H → EReal) (u : H) (hf : HasContinuousAffineMinorantWithSlope f u) (hg : HasContinuousAffineMinorantWithSlope g u) (x : H) : (fun (f g : H → EReal) (x : H) => infimalConvolution (fun (y : H) => f y) (fun (y : H) => g y) x) f g x ≠ ⊥

Under the hypotheses of Proposition 12.6 (i), the infimal convolution never attains -∞.

theorem ERealFunction.infimalConvolution_assoc_of_commonSlopeMinorants {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (f g h : H → EReal) (u : H) (hf : HasContinuousAffineMinorantWithSlope f u) (hg : HasContinuousAffineMinorantWithSlope g u) (hh : HasContinuousAffineMinorantWithSlope h u) : infimalConvolution f (infimalConvolution g h) = infimalConvolution (infimalConvolution f g) h

Proposition 12.6 (iv): if f, g, and h admit continuous affine minorants with the same slope, then infimal convolution is associative on f, g, and h.