Interpolation of parallel convex sets

For convex sets A and B, Minkowski addition and nonnegative scalar multiplication commute with weighted interpolation:

p • (A + s • B) + q • (A + t • B) = A + (p * s + q * t) • B

when p + q = 1. Thus the family of outer parallel sets A + t • B is affine under Minkowski interpolation. The specialization where B is the closed unit ball is the set identity used to transfer Brunn--Minkowski concavity to the volumes of outer parallel bodies.

No nonemptiness or topological assumptions are needed: the result is an algebraic consequence of convexity, combined with Mathlib's distributivity smul_add of scalar multiplication over pointwise set addition.

Main results

• Convex.add_smul_interpolation: interpolation of two parallel convex sets with arbitrary nonnegative weights summing to one.
• Convex.add_smul_interpolation_sub: the same identity with weights 1 - u and u.

theorem Convex.add_smul_interpolation {𝕜 : Type u_1} {E : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {A B : Set E} (hA : Convex 𝕜 A) (hB : Convex 𝕜 B) {p q s t : 𝕜} (hp : 0 ≤ p) (hq : 0 ≤ q) (hpq : p + q = 1) (hs : 0 ≤ s) (ht : 0 ≤ t) : p • (A + s • B) + q • (A + t • B) = A + (p * s + q * t) • B

Weighted interpolation between the parallel convex sets A + s • B and A + t • B is the parallel set at the correspondingly weighted parameter.

theorem Convex.add_smul_interpolation_sub {𝕜 : Type u_1} {E : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {A B : Set E} (hA : Convex 𝕜 A) (hB : Convex 𝕜 B) {u s t : 𝕜} (hu : u ∈ Set.Icc 0 1) (hs : 0 ≤ s) (ht : 0 ≤ t) : (1 - u) • (A + s • B) + u • (A + t • B) = A + ((1 - u) * s + u * t) • B

Convex-combination form of Convex.add_smul_interpolation, parametrized by u ∈ [0, 1].